|
1227
|
1 |
(* ID: $Id$
|
|
|
2 |
Author: Mateja Jamnik, University of Cambridge
|
|
|
3 |
Copyright 1995 University of Cambridge
|
|
|
4 |
|
|
|
5 |
Convert the Isabelle theory files to .html format for hypertext browsing
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
val htmlpath = "/homes/lcp/html_isa/";
|
|
|
9 |
|
|
|
10 |
(* --------------------
|
|
|
11 |
Exception declaration in case that there is a lexical
|
|
|
12 |
error occurs.
|
|
|
13 |
-------------------- *)
|
|
|
14 |
|
|
|
15 |
exception lex_err;
|
|
|
16 |
|
|
|
17 |
(* --------------------
|
|
|
18 |
Get the list of all the theory files and the
|
|
|
19 |
path to access them in their directories
|
|
|
20 |
-------------------- *)
|
|
|
21 |
|
|
|
22 |
print_depth 1000;
|
|
|
23 |
val theory_list = !loaded_thys;
|
|
|
24 |
val files = Symtab.alist_of (theory_list);
|
|
|
25 |
|
|
|
26 |
(* --------------------
|
|
|
27 |
The function move_eachf is going to move all the theory
|
|
|
28 |
files in isabelle to their html format. It takes
|
|
|
29 |
for arguments the name of the theory (tname) and
|
|
|
30 |
other theory information such as path (path), theorems (thms)
|
|
|
31 |
proved, ... It is the main driver of the program, and basically
|
|
|
32 |
contains all other functions. It contains the following
|
|
|
33 |
subfunctions:
|
|
|
34 |
- create_pure
|
|
|
35 |
- gettext
|
|
|
36 |
- move_onef
|
|
|
37 |
- transform
|
|
|
38 |
-------------------- *)
|
|
|
39 |
|
|
|
40 |
fun move_eachf (tname, ThyInfo{path,thms,...}) =
|
|
|
41 |
let val intext = path^tname^".thy";
|
|
|
42 |
val outtext = htmlpath^tname^".html";
|
|
|
43 |
|
|
|
44 |
(* --------------------
|
|
|
45 |
The function gettext takes an instrem from the auxilliary
|
|
|
46 |
file .thy whose name and path are specified in the existent
|
|
|
47 |
Isabelle structure, treats the inputted string with all the
|
|
|
48 |
necessary modifications for html format and puts it into the
|
|
|
49 |
file with the same name but .html extension. The subfunctions
|
|
|
50 |
it contains are:
|
|
|
51 |
- after_first_c
|
|
|
52 |
- filter
|
|
|
53 |
- first_comment
|
|
|
54 |
- format_link
|
|
|
55 |
- getstring
|
|
|
56 |
- get_word
|
|
|
57 |
- he
|
|
|
58 |
- html
|
|
|
59 |
- html_escape
|
|
|
60 |
- insert_link
|
|
|
61 |
- leading_comment
|
|
|
62 |
- lc_exists
|
|
|
63 |
- modify_body
|
|
|
64 |
- remove_lc
|
|
|
65 |
- rest
|
|
|
66 |
- thy_name
|
|
|
67 |
-------------------- *)
|
|
|
68 |
|
|
|
69 |
fun gettext is =
|
|
|
70 |
let
|
|
|
71 |
val head = "<HTML>\n<HEAD>\n<TITLE>"^intext^
|
|
|
72 |
"</TITLE>\n</HEAD>\n\n"^"<BODY>\n";
|
|
|
73 |
val title = "<H1>"^tname^".thy"^"</H1></P>\n\n"^
|
|
|
74 |
"<BR>\n<A HREF = \""^htmlpath^
|
|
|
75 |
"00-chart.html\">Dependency Chart</A>\n"^
|
|
|
76 |
": display of dependencies between the theories.\n"^
|
|
|
77 |
"<BR>\n<HR>\n\n<PRE>\n";
|
|
|
78 |
val tail = "</PRE>"^"</BODY>\n"^"</HTML>";
|
|
|
79 |
|
|
|
80 |
|
|
|
81 |
(* --------------------
|
|
|
82 |
The function he (html escape) is going to take
|
|
|
83 |
every single characterof the input stream and check
|
|
|
84 |
for ">", "<" and "&" characters that have a special
|
|
|
85 |
meaning in html and convert them into their corresponding
|
|
|
86 |
escape sequences.
|
|
|
87 |
-------------------- *)
|
|
|
88 |
fun he [] r = r
|
|
|
89 |
| he ("<"::sl) r = he sl (r@["&","l","t"])
|
|
|
90 |
| he (">"::sl) r = he sl (r@["&","g","t"])
|
|
|
91 |
| he ("&"::sl) r = he sl (r@["&","a","m","p"])
|
|
|
92 |
| he (c::sl) r = he sl (r@[c]);
|
|
|
93 |
|
|
|
94 |
fun html_escape sl = he sl [];
|
|
|
95 |
|
|
|
96 |
(* --------------------
|
|
|
97 |
The function first_comment is a pattern checking for
|
|
|
98 |
nested comments. The argument d will keep track of how
|
|
|
99 |
deep we are in the nested comment. The function will
|
|
|
100 |
return the first comment extracted from the input stream,
|
|
|
101 |
so that we can copy it into the output stream. Lexical
|
|
|
102 |
error is raised if we open an empty file to read from.
|
|
|
103 |
-------------------- *)
|
|
|
104 |
fun first_comment ("*"::")"::cs) co 1 = co@["*",")"]
|
|
|
105 |
| first_comment ("*"::")"::cs) co d =
|
|
|
106 |
first_comment cs (co@["*",")"]) (d-1)
|
|
|
107 |
| first_comment ("("::"*"::cs) co d =
|
|
|
108 |
first_comment cs (co@["(","*"]) (d+1)
|
|
|
109 |
| first_comment (c::cs) co d =
|
|
|
110 |
if d>0 then first_comment cs (co@[c]) d
|
|
|
111 |
else first_comment cs co d
|
|
|
112 |
| first_comment [] _ _ = raise lex_err;
|
|
|
113 |
|
|
|
114 |
(* --------------------
|
|
|
115 |
The function lc_exists leading comment exists?)
|
|
|
116 |
checks whether in the input file at the very beginning
|
|
|
117 |
there is a comment, which needs to be extracted and put
|
|
|
118 |
into the output file. We also need to check whether there
|
|
|
119 |
might be a space, a new line or a tab, which do not
|
|
|
120 |
exclude the possibility that there is a leading comment.
|
|
|
121 |
The function returns a boolean value.
|
|
|
122 |
-------------------- *)
|
|
|
123 |
fun lc_exists ("("::"*"::_) = true
|
|
|
124 |
| lc_exists (" "::cs) = lc_exists cs
|
|
|
125 |
| lc_exists ("\n"::cs) = lc_exists cs
|
|
|
126 |
| lc_exists ("\t"::cs) = lc_exists cs
|
|
|
127 |
| lc_exists _ = false;
|
|
|
128 |
|
|
|
129 |
(* --------------------
|
|
|
130 |
In the case that there is a leading comment, this
|
|
|
131 |
function leading_comment extracts it> It also need
|
|
|
132 |
to check for any html escape sequences in the comment.
|
|
|
133 |
-------------------- *)
|
|
|
134 |
fun leading_comment sl =
|
|
|
135 |
if (lc_exists sl) then
|
|
|
136 |
(html_escape (first_comment sl [] 0))
|
|
|
137 |
else
|
|
|
138 |
[""];
|
|
|
139 |
|
|
|
140 |
(* --------------------
|
|
|
141 |
The function thy_name checks for the parent theory
|
|
|
142 |
names apearing after the leading comment. The function
|
|
|
143 |
returns a boolean value indicating if the word is a
|
|
|
144 |
theory name, so that a link can be inserted and can look
|
|
|
145 |
for another potential theory name. If the word is not a
|
|
|
146 |
theory name then continue to modify the rest of the body.
|
|
|
147 |
-------------------- *)
|
|
|
148 |
fun thy_name word =
|
|
|
149 |
is_some (Symtab.lookup (theory_list, word));
|
|
|
150 |
|
|
|
151 |
(* --------------------
|
|
|
152 |
Creates the right html format when inserting the link.
|
|
|
153 |
-------------------- *)
|
|
|
154 |
fun format_link s =
|
|
|
155 |
let in
|
|
|
156 |
output(std_out,"\n"^s);
|
|
|
157 |
"<A HREF = \""^htmlpath^s^".html\">"^s^"</A>"
|
|
|
158 |
end;
|
|
|
159 |
|
|
|
160 |
(* --------------------
|
|
|
161 |
-------------------- *)
|
|
|
162 |
|
|
|
163 |
fun insert_link w = (explode (format_link (implode w)))
|
|
|
164 |
(* --------------------
|
|
|
165 |
-------------------- *)
|
|
|
166 |
|
|
|
167 |
fun html ( " "::l) r = html l (r@[ " "])
|
|
|
168 |
| html ( "+"::l) r = html l (r@[ "+"])
|
|
|
169 |
| html ("\n"::l) r = html l (r@["\n"])
|
|
|
170 |
| html ("\t"::l) r = html l (r@["\t"])
|
|
|
171 |
| html l r = r@(get_word l [])
|
|
|
172 |
(* --------------------
|
|
|
173 |
-------------------- *)
|
|
|
174 |
and get_word ( " "::l) w =
|
|
|
175 |
if (thy_name (implode w))
|
|
|
176 |
then (insert_link w)@[ " "]@(html l [])
|
|
|
177 |
else w@[" "]@(html_escape l)
|
|
|
178 |
| get_word ( "+"::l) w =
|
|
|
179 |
if (thy_name (implode w))
|
|
|
180 |
then (insert_link w)@[ "+"]@(html l [])
|
|
|
181 |
else w@["+"]@(html_escape l)
|
|
|
182 |
| get_word ("\n"::l) w =
|
|
|
183 |
if (thy_name (implode w))
|
|
|
184 |
then (insert_link w)@[ "\n"]@(html l [])
|
|
|
185 |
else w@["\n"]@(html_escape l)
|
|
|
186 |
| get_word ("\t"::l) w =
|
|
|
187 |
if (thy_name (implode w))
|
|
|
188 |
then (insert_link w)@[ "\t"]@(html l [])
|
|
|
189 |
else w@["\t"]@(html_escape l)
|
|
|
190 |
| get_word (c::l) w = (get_word l (w@[c]))
|
|
|
191 |
| get_word [] [] = []
|
|
|
192 |
| get_word [] w =
|
|
|
193 |
if (thy_name (implode w))
|
|
|
194 |
then (insert_link w)
|
|
|
195 |
else w;
|
|
|
196 |
|
|
|
197 |
(* --------------------
|
|
|
198 |
-------------------- *)
|
|
|
199 |
fun modify_body ("="::l) r = r@["="]@(html l [])
|
|
|
200 |
| modify_body (c::l) r = modify_body l (r@[c])
|
|
|
201 |
| modify_body [] r = r;
|
|
|
202 |
|
|
|
203 |
(* --------------------
|
|
|
204 |
-------------------- *)
|
|
|
205 |
fun after_first_c ("*"::")"::cs) 1 = cs
|
|
|
206 |
| after_first_c ("*"::")"::cs) d = after_first_c cs (d-1)
|
|
|
207 |
| after_first_c ("("::"*"::cs) d = after_first_c cs (d+1)
|
|
|
208 |
| after_first_c (c::cs) d = after_first_c cs d
|
|
|
209 |
| after_first_c cs 0 = cs
|
|
|
210 |
| after_first_c [] _ = raise lex_err;
|
|
|
211 |
|
|
|
212 |
(* --------------------
|
|
|
213 |
-------------------- *)
|
|
|
214 |
fun remove_lc sl =
|
|
|
215 |
if (lc_exists sl) then (after_first_c sl 0) else sl;
|
|
|
216 |
|
|
|
217 |
(* --------------------
|
|
|
218 |
-------------------- *)
|
|
|
219 |
fun rest sl = modify_body (remove_lc sl) [];
|
|
|
220 |
|
|
|
221 |
(* --------------------
|
|
|
222 |
-------------------- *)
|
|
|
223 |
fun filter sl = (leading_comment sl) @ (rest sl);
|
|
|
224 |
|
|
|
225 |
(* --------------------
|
|
|
226 |
-------------------- *)
|
|
|
227 |
fun getstring s =
|
|
|
228 |
case input (is, 1) of
|
|
|
229 |
"" => head^title^(implode(filter(explode(s))))^tail
|
|
|
230 |
| "\n" => getstring (s^"\n")
|
|
|
231 |
| c => getstring (s^c)
|
|
|
232 |
in
|
|
|
233 |
getstring ""
|
|
|
234 |
end;
|
|
|
235 |
|
|
|
236 |
(* --------------------
|
|
|
237 |
-------------------- *)
|
|
|
238 |
fun transform t =
|
|
|
239 |
let
|
|
|
240 |
val infile = open_in intext;
|
|
|
241 |
val outfile = open_out outtext
|
|
|
242 |
in
|
|
|
243 |
output(std_out,"\nTheory: "^t);
|
|
|
244 |
output (outfile, gettext(infile));
|
|
|
245 |
close_in (infile);
|
|
|
246 |
close_out (outfile)
|
|
|
247 |
end;
|
|
|
248 |
|
|
|
249 |
(* --------------------
|
|
|
250 |
-------------------- *)
|
|
|
251 |
fun create_pure p =
|
|
|
252 |
let
|
|
|
253 |
val outfile = open_out outtext
|
|
|
254 |
in
|
|
|
255 |
output(std_out, "\nCreating Pure.html ...");
|
|
|
256 |
output (outfile, "<HTML>\n<HEAD>\n<TITLE>"^intext^
|
|
|
257 |
"</TITLE>\n</HEAD>\n\n"^"<BODY>\n"^
|
|
|
258 |
"<H1>"^tname^".thy"^"</H1></P>\n\n"^"<PRE>\n"^
|
|
|
259 |
"This is a theory file called Pure.\n"^
|
|
|
260 |
"Its children are all other Isabelle theories."^
|
|
|
261 |
"</PRE>"^"</BODY>\n"^"</HTML>");
|
|
|
262 |
close_out (outfile)
|
|
|
263 |
end
|
|
|
264 |
|
|
|
265 |
in
|
|
|
266 |
if (tname <> "Pure") then (transform tname)
|
|
|
267 |
else (create_pure tname)
|
|
|
268 |
end;
|
|
|
269 |
|
|
|
270 |
(* --------------------
|
|
|
271 |
-------------------- *)
|
|
|
272 |
map move_eachf (files);
|
|
|
273 |
|