1(* Htmlsigs: some hacks to turn Moscow ML annotated signature files into 2 HTML-files. Peter Sestoft 1997-05-08, 1997-07-31, 2000-01-10, 2000-06-01 3*) 4structure Htmlsigs :> Htmlsigs = struct 5fun indexbar out srcpath = out (String.concat 6 ["<hr><table width=\"100%\">", 7 "<tr align = center>\n", 8 "<th><a href=\"file://", srcpath, 9 "\" type=\"text/plain\">Source File</a>\n", 10 "<th><a href=\"idIndex.html\">Identifier index</A>\n", 11 "<th><a href=\"TheoryIndex.html\">Theory binding index</A>\n", 12 "</table><hr>\n"]); 13 14val smlIdCharSym = Char.contains "'_!%&$#+-/:<=>?@\\~`^|*" 15fun smlIdChar c = Char.isAlphaNum c orelse smlIdCharSym c 16 17fun destProperSuffix s1 s2 = 18 let val sz1 = String.size s1 19 val sz2 = String.size s2 20 open Substring 21 in 22 if sz1 >= sz2 then NONE 23 else let val (prefix, suffix) = splitAt(full s2, sz2 - sz1) 24 in if string suffix = s1 then SOME (string prefix) else NONE 25 end 26 end; 27 28fun isTheorysig path = 29 let open OS.Path 30 val {dir,file} = splitDirFile path 31 val {base,ext} = splitBaseExt file 32 in ext=SOME "sig" andalso Option.isSome (destProperSuffix "Theory" base) 33 end 34 handle _ => false; 35 36fun assoc item = 37 let fun assc ((key,ob)::rst) = if item=key then ob else assc rst 38 | assc [] = raise Fail ("assoc: "^item^" not found") 39 in assc 40 end 41 42fun find_most_appealing HOLpath docfile = 43 let open OS.Path OS.FileSys 44 val {dir,file} = splitDirFile docfile 45 val {base,ext} = splitBaseExt file 46 val docfile_dir = concat(HOLpath,dir) 47 val htmldir = concat(docfile_dir,"HTML") 48 val htmlfile = joinBaseExt{base=base,ext=SOME "html"} 49 val adocfile = joinBaseExt{base=base,ext=SOME "txt"} 50 val htmlpath = concat(htmldir,htmlfile) 51 val adocpath = concat(docfile_dir,adocfile) 52 val docpath = concat(docfile_dir,file) 53 in 54 if OS.FileSys.access(htmlpath,[A_READ]) then SOME htmlpath else 55 if OS.FileSys.access(adocpath,[A_READ]) then SOME adocpath else 56 if OS.FileSys.access(file,[A_READ]) then SOME docpath 57 else NONE 58 end; 59 60fun processSig db version bgcolor HOLpath SRCFILES sigfile htmlfile = 61 let val strName = OS.Path.base (OS.Path.file sigfile) 62 val is = TextIO.openIn sigfile 63 val lines = Substring.fields (fn c => c = #"\n") 64 (Substring.full (TextIO.inputAll is)) 65 val _ = TextIO.closeIn is 66 67 fun comp2str comp = 68 let open Database 69 in 70 case comp of 71 Exc _ => "exc" 72 | Typ _ => "typ" 73 | Con _ => "con" 74 | Val _ => "val" 75 | Str => "str" 76 | Term _ => "ter" 77 end 78 79 (* Skip 'tyvar and ('tyvar, ..., 'tyvar), return the id that 80 follows *) 81 82 fun scanident getc src = 83 let open StringCvt 84 fun isn't c1 c2 = c1 <> c2 85 fun is c1 c2 = c1 = c2 86 val sus1 = skipWS getc src 87 fun readident sus = 88 splitl smlIdChar getc (skipWS getc sus) 89 in 90 case getc sus1 of 91 SOME(#"'", sus2) => 92 let val sus3 = dropl (not o Char.isSpace) getc sus2 93 in readident sus3 end 94 | SOME(#"(", sus2) => 95 let val sus3 = dropl (isn't #")") getc sus2 96 val sus4 = dropl (is #")") getc sus3 97 in readident sus4 end 98 | SOME _ => readident sus1 99 | NONE => readident sus1 100 end 101 102 val scanident = scanident Substring.getc 103 104 fun definition susline isntdef isdef = 105 let open Database Substring 106 val (id, after) = scanident (triml 4 susline) 107 fun relevant {file, ...} = file=strName 108 val comps = 109 List.map #comp (List.filter relevant (lookup (db, id))) 110 fun linehas s = not (isEmpty (#2 (position s after))) 111 fun indexcomp comp = 112 case comp of 113 Exc i => if i=id then SOME comp else NONE 114 | Typ i => if i=id andalso linehas "type" then SOME comp 115 else NONE 116 | Con i => if i=id then SOME comp else NONE 117 | Val i => if i=id then SOME comp else NONE 118 | Str => if linehas "structure" then SOME comp 119 else NONE 120 | Term _ => SOME comp 121 fun kindof Str = 3 122 | kindof (Val _) = 4 123 | kindof (Typ _) = 1 124 | kindof (Exc _) = 2 125 | kindof (Con _) = 5 126 | kindof (Term _) = 6 127 fun kindCompare (c1, c2) = Int.compare(kindof c1, kindof c2) 128 val comps = Listsort.sort kindCompare 129 (List.mapPartial indexcomp comps) 130 in 131 case comps of 132 [] => isntdef susline (* No def *) 133 | comp :: _ => isdef susline id after comp (* Def *) 134 end 135 136 (* First pass over the file: record anchors of identifier defs *) 137 138 val anchors = ref (Binaryset.empty String.compare) 139 140 fun pass1 susline lineno = 141 let open Substring 142 fun nameanchor _ id _ comp = 143 anchors := (Binaryset.add (!anchors, id ^ "-" ^ comp2str comp)) 144 in 145 if isPrefix " [" susline then 146 definition susline ignore nameanchor 147 else () 148 end 149 150 (* Second pass over the file *) 151 152 val os = TextIO.openOut htmlfile 153 fun out s = TextIO.output(os, s) 154 155 fun encode #"<" = "<" 156 | encode #">" = ">" 157(* | encode #"&" = "&" *) 158 | encode c = str c 159 160 fun outSubstr s = TextIO.output(os, Substring.translate encode s) 161 162 val seenDefinition = ref false 163 164 fun name anchor target = 165 (out "<a name=\""; out target; out "\">"; out anchor; out "</a>") 166 167 fun idhref link id = 168 (out "<a href=\"#"; out link; out "\">"; out id; out"</a>") 169 fun idhref_full link id = 170 (out "<a href=\"file://"; out link; out "\">"; out id; out"</a>") 171 172 fun removeTrailingColon id = 173 let 174 val n = String.size id - 1 175 in 176 if 0 < n andalso String.sub (id, n) = #":" 177 then String.substring (id, 0, n) 178 else id 179 end 180 181 val aliasStrName = 182 fn "DefinitionDoc" => "Definition" 183 | "FinalType" => "Type" 184 | "FinalTerm" => "Term" 185 | "FinalThm" => "Thm" 186 | "HolKernelDoc" => "HolKernel" 187 | s => s 188 189 fun locate_docfile id = 190 let open OS.FileSys OS.Path Database 191 val id = removeTrailingColon id 192 val qualid = aliasStrName strName ^ "." ^ id 193 fun trav [] = NONE 194 | trav({comp=Database.Term(x,SOME "HOL"),file,line}::rst) 195 = if x=qualid 196 then find_most_appealing HOLpath file 197 else trav rst 198 | trav (_::rst) = trav rst 199 in 200 Option.map (fn x => (x, id)) (trav (lookup(db,id))) 201 end 202 203 fun declaration isThryFile lineno space1 decl kindtag = 204 let open Substring 205 fun isKind c = Char.isAlpha c orelse c = #"_" 206 val (kind, rest) = splitl isKind decl 207 val (id, after) = scanident rest 208 val preflen = size decl - size after - String.size id 209 val preid = slice(decl, 0, SOME preflen) 210 val link = id ^ "-" ^ kindtag 211 in 212 outSubstr space1; 213 outSubstr preid 214 ; 215 if id = "" then () 216 else if not (Binaryset.member (!anchors, link)) 217 then if isThryFile then out id (* shouldn't happen *) 218 else case locate_docfile id 219 of NONE => out id 220 | SOME (file, id2) => 221 (idhref_full file id2 222 ; if id <> id2 then out ":" else ()) 223 else idhref link id 224 ; 225 outSubstr after 226 end 227 228 (* Format susline which defines identifier id of kind comp: *) 229 230 fun outisdef susline id after comp = 231 let open Substring 232 fun namebold id s = 233 (out "<a name=\""; out id; out "-"; out s; 234 out "\"><b>"; out id; out "</b></a>") 235 val preflen = size susline - size after - String.size id 236 val pref = slice(susline, 0, SOME preflen) 237 in 238 outSubstr pref; namebold id (comp2str comp); 239 outSubstr after 240 end 241 242 fun pass2 isThryFile susline lineno = 243 let open Substring 244 in 245 (if isPrefix " [" susline 246 then (definition susline outSubstr outisdef; 247 seenDefinition := true) 248 else if not (!seenDefinition) then 249 (name "" ("line" ^ Int.toString lineno); 250 let val (space, suff) = splitl Char.isSpace susline 251 val dec = declaration isThryFile lineno space suff 252 in 253 if isPrefix "val " suff 254 orelse isPrefix "prim_val " suff then 255 dec "val" 256 else if isPrefix "prim_type " suff 257 orelse isPrefix "prim_EQtype " suff 258 orelse isPrefix "type " suff 259 orelse isPrefix "eqtype " suff 260 orelse isPrefix "datatype " suff then 261 dec "typ" 262 else if isPrefix "structure " suff then 263 dec "str" 264 else if isPrefix "exception " suff then 265 dec "exc" 266 else 267 outSubstr susline 268 end) 269 else 270 outSubstr susline); 271 out "\n" 272 end 273 274 fun traverse process = 275 let fun loop [] lineno = () 276 | loop (ln::lnr) lineno = 277 (process ln lineno; loop lnr (lineno+1)) 278 in loop lines 1 end 279 280 val srcfile = assoc (OS.Path.base(OS.Path.file sigfile)) SRCFILES 281 in 282 (*print "Creating "; print htmlfile; print " from "; 283 print sigfile; print "\n" 284 ; *) 285 traverse pass1; 286 out "<!DOCTYPE html>\n"; 287 out "<html><head>\n"; 288 out "<meta charset=\"utf-8\">\n"; 289 out "<title>Structure "; 290 out strName; out "</title>\n"; 291 out "<style type=\"text/css\">\n"; 292 out "<!--\n"; 293 out " body {background: "; out bgcolor; out "}\n-->\n</style>"; 294 out "</head>\n"; 295 out "<body>\n"; 296 out "<h1>Structure "; out strName; out "</h1>\n"; 297 indexbar out srcfile; 298 out "<pre>\n"; 299 traverse (pass2 (isTheorysig sigfile)); 300 out "</pre>"; 301 indexbar out srcfile; 302 out "<p><em>"; out version; out "</em></p>"; 303 out "</body></html>\n"; 304 TextIO.closeOut os 305 end 306 307fun processSigfile db version bgcolor stoplist 308 sigdir htmldir HOLpath SRCFILES sigfile = 309 let val {base, ext} = OS.Path.splitBaseExt sigfile 310 val htmlfile = OS.Path.joinBaseExt{base=base, ext=SOME "html"} 311 in 312 case ext 313 of SOME "sig" => 314 if List.exists (fn name => base = name) stoplist then () 315 else processSig db version bgcolor HOLpath SRCFILES 316 (OS.Path.concat(sigdir, sigfile)) 317 (OS.Path.concat(htmldir, htmlfile)) 318 | otherwise => () 319 end 320 321fun listDir s = let 322 val ds = OS.FileSys.openDir s 323 fun recurse acc = 324 case OS.FileSys.readDir ds of 325 NONE => acc 326 | SOME f => recurse (f :: acc) 327in 328 recurse [] before OS.FileSys.closeDir ds 329end 330 331fun sigsToHtml version bgcolor stoplist 332 helpfile HOLpath SRCFILES (sigdir, htmldir) = 333 let open OS.FileSys Database 334 val db = readbase helpfile 335 fun mkdir htmldir = 336 if access(htmldir, [A_WRITE, A_EXEC]) andalso isDir htmldir then 337 (print "Directory "; print htmldir; print " exists\n") 338 else 339 (OS.FileSys.mkDir htmldir; 340 print "Created directory "; print htmldir; print "\n"); 341 in 342 mkdir htmldir; 343 app (processSigfile db version bgcolor 344 stoplist sigdir htmldir HOLpath SRCFILES) 345 (listDir sigdir) 346 end 347 handle exn as OS.SysErr (str, _) => (print(str ^ "\n\n"); raise exn) 348 349fun printHTMLBase version bgcolor HOLpath pred header (sigfile, outfile) = 350 let open Database 351 val db = readbase sigfile 352 val os = TextIO.openOut outfile 353 fun out s = TextIO.output(os, s) 354 fun href anchor target = 355 app out ["<a href=\"", target, "\">", anchor, "</a>"] 356 fun idhref file line anchor = 357 href anchor (concat [file, ".html#line", Int.toString line]) 358 fun strhref file anchor = 359 href anchor (file ^ ".html") 360 fun mkalphaindex seps = 361 (out "<hr>\n<center><b>"; 362 List.app 363 (fn c => (href (str c) ("#" ^ str c); out " ")) 364 seps; 365 out "</b></center><hr>\n") 366 fun subheader txt = app out ["\n<h2>", txt, "</h2>\n"] 367 368 (* Insert a subheader when meeting a new initial letter *) 369 val lastc1 = ref #" " 370 val firstsymb = ref true 371 fun separator k1 = 372 let val c1 = Char.toUpper k1 373 in 374 if Char.isAlpha c1 andalso c1 <> !lastc1 then 375 (lastc1 := c1; 376 app out ["\n</ul>\n\n<a name=\"", str c1, "\">"]; 377 subheader (str c1); 378 out "</a>\n<ul>") 379 else if !firstsymb andalso not (Char.isAlpha c1) 380 then (subheader "Symbolic Identifiers"; 381 out "<ul>"; 382 firstsymb := false) 383 else () 384 end 385 fun mkref line file = idhref file line file 386 fun mkHOLref docfile = 387 case find_most_appealing HOLpath docfile 388 of SOME file => href "Docfile" file 389 | NONE => out "not linked" 390 fun nextfile last [] = out ")\n" 391 | nextfile last ((e1 as {comp, file, line}) :: erest) = 392 if comp=last then (out ", "; mkref line file; nextfile last erest) 393 else (out ")\n"; newitem e1 erest) 394 and newitem (e1 as {comp, file, line}) erest = 395 let val key = Database.getname e1 396 in separator (String.sub(key, 0)) 397 ; out "<li><b>"; out key; out "</b> (" 398 ; (case comp 399 of Str => strhref key "structure" 400 | Val id => (out "value; "; mkref line file) 401 | Typ id => (out "type; "; mkref line file) 402 | Exc id => (out "exception; "; mkref line file) 403 | Con id => (out "constructor; "; mkref line file) 404 | Term (id, NONE) => mkref line file 405(* | Term (id, SOME "HOL") => (out "HOL; "; mkHOLref file) *) 406 | Term (id, SOME kind) => (out kind;out"; ";mkref line file) 407 ; nextfile comp erest) 408 end 409 fun prentries [] = () 410 | prentries (e1 :: erest) = newitem e1 erest 411 fun prtree Empty = () 412 | prtree (Node(key, entries, t1, t2)) = 413 (prtree t1; 414 prentries (List.filter pred entries); 415 prtree t2) 416 417 (* Get list of initial letters *) 418 fun separators Empty l = l 419 | separators (Node(key, entries, t1, t2)) l = 420 separators t2 (separators t1 421 (let val k = Char.toUpper (String.sub(key, 0)) in 422 if Char.isAlpha k andalso 423 not (null (List.filter pred entries)) andalso 424 not (Option.isSome (List.find (fn x => x = k) l)) 425 then 426 k :: l 427 else 428 l 429 end)) 430 val seps = Listsort.sort Char.compare (separators db []) 431 in 432 out "<!DOCTYPE html><html><head><meta charset=\"utf-8\"><title>"; out header; out "</title></head>\n"; 433 out "<body bgcolor=\""; out bgcolor; out "\">\n"; 434 out "<h1>"; out header; out "</h1>\n"; 435 mkalphaindex seps; 436 prtree db; 437 out "</ul>\n"; 438 mkalphaindex seps; 439 out "<p><em>"; out version; out "</em></p>"; 440 out "</body></html>\n"; 441 TextIO.closeOut os 442 end 443end 444