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 "&nbsp;&nbsp;&nbsp;&nbsp;\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 "&nbsp;&nbsp;&nbsp;\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 "&nbsp;&nbsp;&nbsp;&nbsp;";
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