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 "<" 30 | txt_helper #">" = SOME ">" 31 | txt_helper #"&" = SOME "&" 32 | txt_helper c = NONE 33 34fun encode c = Option.getOpt(txt_helper c, String.str c) 35fun brkt_encode #" " = " " 36 | brkt_encode c = encode c 37 38fun text_encode ss = let 39 (* passes over a substring, replacing single apostrophes with ’ 40 backquotes with ‘ and the "latex" encodings of nice double-quotes: 41 `` with “ and '' with ” 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) => ("‘" :: acc) 48 | (apostrophe, NONE) => ("’" :: 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 ("”" :: acc) (normal(0,ss')) ss' 64 | (apostrophe, SOME(#"`", ss')) => 65 recurse ("’" :: acc) backquote ss' 66 | (apostrophe, SOME _) => 67 recurse ("’" :: acc) (normal(0,ss)) ss 68 | (backquote, SOME(#"`", ss')) => 69 recurse ("“" :: acc) (normal(0,ss')) ss' 70 | (backquote, SOME(#"'", ss')) => 71 recurse ("‘" :: acc) apostrophe ss' 72 | (backquote, SOME _) => 73 recurse ("‘" :: 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> "; 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