1structure HOLPage = struct 2open Database; 3 4fun equal x y = (x=y); 5fun curry f x y = f (x,y); 6 7fun itstrings f [] = raise Fail "itstrings: empty list" 8 | itstrings f [x] = x 9 | itstrings f (h::t) = f h (itstrings f t); 10 11val normPath = (* string list -> string *) 12 OS.Path.toString o OS.Path.fromString o itstrings (curry OS.Path.concat); 13 14fun destProperSuffix s1 s2 = 15 let val sz1 = String.size s1 16 val sz2 = String.size s2 17 open Substring 18 in 19 if sz1 >= sz2 then NONE 20 else let val (prefix, suffix) = splitAt(full s2, sz2 - sz1) 21 in if string suffix = s1 then SOME (string prefix) else NONE 22 end 23 end; 24 25val dropTheory = destProperSuffix "Theory"; 26val dropLib = destProperSuffix "Lib"; 27val dropSyntax = destProperSuffix "Syntax"; 28val dropSimps = destProperSuffix "Simps"; 29 30fun find_most_appealing HOLpath docfile = 31 let open OS.Path OS.FileSys 32 val {dir,file} = splitDirFile docfile 33 val {base,ext} = splitBaseExt file 34 val docfile_dir = concat(HOLpath,dir) 35 val htmldir = concat(docfile_dir,"HTML") 36 val htmlfile = joinBaseExt{base=base,ext=SOME "html"} 37 val adocfile = joinBaseExt{base=base,ext=SOME "txt"} 38 val htmlpath = normPath[htmldir,htmlfile] 39 val adocpath = normPath[docfile_dir,adocfile] 40 val docpath = normPath[docfile_dir,file] 41 in 42 if OS.FileSys.access(htmlpath,[A_READ]) then SOME htmlpath else 43 if OS.FileSys.access(adocpath,[A_READ]) then SOME adocpath else 44 if OS.FileSys.access(file,[A_READ]) then SOME docpath 45 else NONE 46 end; 47 48fun printHOLPage version bgcolor HOLpath idIndex TheoryIndex (dbfile, outfile) 49 = let val db = readbase dbfile 50 val os = TextIO.openOut outfile 51 fun out s = TextIO.output(os, s) 52 fun href anchor target = 53 app out ["<A HREF=\"file://", target, "\">", anchor, "</A>"] 54 fun idhref file line anchor = 55 href anchor (concat [file, ".html#line", Int.toString line]) 56 fun strhref file anchor = href anchor (file ^ ".html") 57 fun mkref line file = idhref file line file 58 val sigspath = normPath[HOLpath,"help","src-sml","htmlsigs"] 59 fun path front file = normPath[front, file^".html"] 60 61 fun class_of drop {comp=Str, file, line} = 62 (case drop file 63 of SOME name => SOME(name, path sigspath file) 64 | NONE => NONE) 65 | class_of _ otherwise = NONE 66 67 val theory_of = class_of dropTheory 68 val library_of = class_of dropLib 69 val syntax_of = class_of dropSyntax 70 val simps_of = class_of dropSimps 71 72 fun misc_struct_of {comp=Str, file, line} = 73 if isSome (dropTheory file) orelse 74 isSome (dropLib file) orelse 75 isSome (dropSyntax file) orelse 76 isSome (dropSimps file) 77 then NONE 78 else SOME(file, path sigspath file) 79 | misc_struct_of otherwise = NONE 80 81 fun prentries [] = () 82 | prentries ((anchor,path)::rst) = 83 let 84 in href anchor path 85 ; out " \n" 86 ; prentries rst 87 end 88 fun prtree f Empty = () 89 | prtree f (Node(key, entries, t1, t2)) = 90 (prtree f t1; 91 prentries (List.mapPartial f entries); 92 prtree f t2) 93 in 94 out "<HTML>\ 95 \<HEAD><TITLE>HOL Reference Page</TITLE></HEAD>\n"; 96 out "<BODY BGCOLOR=\""; out bgcolor; out "\">\n"; 97 out "<H1>HOL Reference Page</H1>\n"; 98 99 out "<DL>"; 100 101 out"<DT><STRONG>LIBRARIES</STRONG>"; 102 out"<DD>"; prtree library_of db; 103 out "<P>"; 104 105 out"<DT><STRONG>THEORIES</STRONG>\n"; 106 out " \n"; 107 href "(Theory Graph)" 108 (normPath [HOLpath,"help/theorygraph/theories.html"]); 109 out "\n"; 110 out"<DD>"; prtree theory_of db; 111 out "<P>"; 112 113 out "<DT><STRONG>STRUCTURES</STRONG>"; 114 out "<DD>"; prtree misc_struct_of db; 115 out "<P>"; 116 117 out"<DT><STRONG>SYNTAX</STRONG>"; 118 out"<DD>"; prtree syntax_of db; 119 out "<P>"; 120 121 out"<DT><STRONG>SIMPLIFICATION SETS</STRONG>"; 122 out"<DD>"; prtree simps_of db; 123 out "<P>"; 124 125 out"<DT><STRONG>"; 126 href "IDENTIFIERS" idIndex; 127 out " "; 128 href "THEORY BINDINGS" TheoryIndex; 129 out "</STRONG>"; 130 out "<P>"; 131 out "</DL>\n"; 132 133 out "<BR><EM>"; out version; out "</EM>"; 134 out "</BODY></HTML>\n"; 135 TextIO.closeOut os 136 end 137end 138