1(*---------------------------------------------------------------------------*)
2(*                                                                           *)
3(*  Invoked with, e.g.,                                                      *)
4(*                                                                           *)
5(*     Doc2Html "/home/kxs/kanan/help/Docfiles"                              *)
6(*              "/home/kxs/kanan/help/Docfiles/html";                        *)
7(*                                                                           *)
8(*---------------------------------------------------------------------------*)
9structure Doc2Html = struct
10
11(* app load ["Substring", "TextIO", "Char", "FileSys"]; *)
12open Substring;
13
14fun curry f x y = f (x,y)
15fun equal x y = (x=y)
16infix ##;
17fun (f##g) (x,y) = (f x, g y);
18
19infixr 4 \/
20infixr 5 /\
21fun (f \/ g) x = f x orelse g x
22fun (f /\ g) x = f x andalso g x;
23
24open ParseDoc
25
26fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n");
27             OS.Process.exit OS.Process.failure)
28
29fun txt_helper #"<" = SOME "&lt;"
30  | txt_helper #">" = SOME "&gt;"
31  | txt_helper #"&" = SOME "&amp;"
32  | txt_helper c = NONE
33
34fun encode c = Option.getOpt(txt_helper c, String.str c)
35fun brkt_encode #" " = "&nbsp;"
36  | brkt_encode c = encode c
37
38fun text_encode ss = let
39  (* passes over a substring, replacing single apostrophes with &rsquo;
40     backquotes with &lsquo; and the "latex" encodings of nice double-quotes:
41     `` with &ldquo; and '' with &rdquo;
42     Also encodes the < > and & characters into HTML appropriate forms. *)
43  open Substring
44  datatype state = backquote | apostrophe | normal of int * substring
45  fun recurse acc s ss =
46      case (s, getc ss) of
47        (backquote, NONE) => ("&lsquo;" :: acc)
48      | (apostrophe, NONE) => ("&rsquo;" :: acc)
49      | (normal(n,ss0), NONE) => (string ss0 :: acc)
50      | (normal (n,ss0), SOME(#"'", ss')) =>
51          recurse (string (slice(ss0,0,SOME n)) :: acc) apostrophe ss'
52      | (normal(n,ss0), SOME(#"`", ss')) =>
53          recurse (string (slice(ss0,0,SOME n))::acc) backquote ss'
54      | (normal(n,ss0), SOME(c, ss')) => let
55        in
56          case txt_helper c of
57            SOME s => recurse (s :: string (slice(ss0,0,SOME n)) :: acc)
58                              (normal(0,ss'))
59                              ss'
60          | NONE => recurse acc (normal(n + 1, ss0)) ss'
61        end
62      | (apostrophe, SOME(#"'", ss')) =>
63          recurse ("&rdquo;" :: acc) (normal(0,ss')) ss'
64      | (apostrophe, SOME(#"`", ss')) =>
65          recurse ("&rsquo;" :: acc) backquote ss'
66      | (apostrophe, SOME _) =>
67          recurse ("&rsquo;" :: acc) (normal(0,ss)) ss
68      | (backquote, SOME(#"`", ss')) =>
69          recurse ("&ldquo;" :: acc) (normal(0,ss')) ss'
70      | (backquote, SOME(#"'", ss')) =>
71          recurse ("&lsquo;" :: acc) apostrophe ss'
72      | (backquote, SOME _) =>
73          recurse ("&lsquo;" :: acc) (normal(0,ss)) ss
74in
75  String.concat (List.rev (recurse [] (normal(0,ss)) ss))
76end
77
78
79fun del_bslash #"\\" = ""
80  | del_bslash c     = String.str c;
81
82(* Location of style sheet *)
83val cssURL = "doc.css";
84
85fun html (name,sectionl) ostrm =
86 let fun outss ss = TextIO.output(ostrm, Substring.translate encode ss)
87     fun out s = TextIO.output(ostrm,s)
88     val bracket_trans = Substring.translate brkt_encode
89     fun markout PARA = out "\n<P>\n"
90       | markout (TEXT ss) =
91            (out "<SPAN class = \"TEXT\">";
92             out  (text_encode ss);
93             out "</SPAN>")
94       | markout (EMPH ss) =
95            out ("<em>" ^ text_encode ss ^ "</em>")
96       | markout (BRKT ss) =
97           (out "<SPAN class = \"BRKT\">";
98            out (bracket_trans ss);
99            out "</SPAN>")
100       | markout (XMPL ss) =
101           (out "<DIV class = \"XMPL\"><pre>";
102            outss ss;
103            out "</pre></DIV>\n")
104
105     fun markout_section (FIELD ("KEYWORDS", _)) = ()
106       | markout_section (FIELD ("DOC", _)) = ()
107       | markout_section (FIELD ("STRUCTURE", [TEXT s]))
108           = (out "<DT><SPAN class = \"FIELD-NAME\">STRUCTURE</SPAN></DT>\n";
109              out "<DD><DIV class = \"FIELD-BODY\">";
110              out "<A HREF = \"../../src-sml/htmlsigs/";
111              out (Symbolic.unsymb(string s)); out ".html\">";
112              out (Symbolic.unsymb(string s));
113              out "</A></DIV></DD>\n")
114       | markout_section (FIELD (tag, ss))
115           = (out "<DT><SPAN class = \"FIELD-NAME\">";
116              out (if tag = "DESCRIBE" then "DESCRIPTION" else tag);
117              out "</SPAN></DT>\n";
118              out "<DD><DIV class = \"FIELD-BODY\">";
119              List.app markout ss;
120              out "</DIV></DD>\n")
121       | markout_section (SEEALSO sslist)
122           = let fun drop_qual ss =
123                 case tokens (equal #".") ss
124                  of [strName,fnName] => translate del_bslash fnName
125                   | [Name] => string Name
126                   | other => raise Fail (string ss)
127                 fun link s =
128                    (out "<A HREF = \"";
129                     out (Symbolic.unsymb(string s)); out ".html\">";
130                     out (drop_qual s); out "</A>")
131                 fun outlinks [] = ()
132                   | outlinks [s] = link s
133                   | outlinks (h::t) = (link h; out",\n"; outlinks t)
134             in
135               (out "<dt><span class = \"FIELD-NAME\">SEEALSO</span></dt>\n";
136                out "<dd><div class = \"FIELD-BODY\">";
137                outlinks sslist;
138                out "</div></dd>\n")
139             end
140       | markout_section (TYPE _) = raise Fail "markout_section: TYPE"
141
142     fun front_matter name (TYPE ss) =
143           (out "<!DOCTYPE html>\n";
144            out "<HTML>\n";
145            out "<HEAD>\n";
146            out "<META CHARSET=\"utf-8\">\n";
147            out "<TITLE>"; out name; out "</TITLE>\n";
148            out "<LINK REL = \"STYLESHEET\" HREF = \"../";
149            out cssURL;
150            out "\" TYPE = \"text/css\">";
151            out "</HEAD>\n";
152            out "<BODY>\n\n";
153            out "<DIV class = \"TYPE\"><PRE>";
154            outss ss;
155            out "</PRE></DIV>\n\n")
156       | front_matter _ _ = raise Fail "front_matter: expected TYPE"
157
158     fun back_matter (www,release) =
159      (out "<div class = \"HOL\"><A HREF=\""; out www;
160       out"\">HOL</A>&nbsp;&nbsp;";
161       out release;
162       out "</div></BODY></HTML>\n")
163
164     val sectionl = tl sectionl
165
166  in
167     front_matter name (hd sectionl);
168     out "<DL>\n";
169     List.app markout_section (tl sectionl);
170     out "</DL>\n\n";
171     back_matter ("http://hol.sourceforge.net",
172                  Systeml.release ^ "-" ^ Int.toString Systeml.version)
173  end;
174
175fun trans htmldir docdir docname = let
176  val docfile = OS.Path.joinBaseExt{base = OS.Path.concat(docdir, docname),
177                                 ext = SOME "doc"}
178  val outfile = OS.Path.joinBaseExt{base = OS.Path.concat(htmldir, docname),
179                                 ext = SOME "html"}
180  val ostrm = TextIO.openOut outfile
181in
182    html (docname, parse_file docfile) ostrm
183  ; TextIO.closeOut ostrm
184end handle e => die ("Exception raised: " ^ General.exnMessage e)
185
186fun docdir_to_htmldir docdir htmldir =
187 let open OS.FileSys
188     val docfiles = ParseDoc.find_docfiles docdir
189     val (tick, finish) = Flash.initialise ("Directory "^docdir^": ",
190                                            Binaryset.numItems docfiles)
191 in
192   Binaryset.app (fn d => (trans htmldir docdir d; tick())) docfiles;
193   finish();
194   OS.Process.exit OS.Process.success
195 end
196
197fun main () =
198  case CommandLine.arguments ()
199     of [docdir,htmldir] => docdir_to_htmldir docdir htmldir
200      | otherwise => print "Usage: Doc2Html <docdir> <htmldir>\n"
201
202end;
203