author | wenzelm |
Wed, 17 Mar 1999 13:40:21 +0100 | |
changeset 6375 | 4bea69e827d0 |
parent 6361 | 3a45ad4a95eb |
child 6388 | ab422f554074 |
permissions | -rw-r--r-- |
6330 | 1 |
(* Title: Pure/Thy/browser_info.ML |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
6330 | 3 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
4 |
||
5 |
Theory browsing information (HTML and graph files). |
|
6 |
*) |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
7 |
|
6330 | 8 |
signature BASIC_BROWSER_INFO = |
9 |
sig |
|
10 |
val section: string -> unit |
|
11 |
end; |
|
3870 | 12 |
|
6330 | 13 |
signature BROWSER_INFO = |
14 |
sig |
|
15 |
include BASIC_BROWSER_INFO |
|
6342 | 16 |
val init: bool -> string list -> string -> unit |
6330 | 17 |
val finish: unit -> unit |
18 |
val theory_source: string -> (string, 'a) Source.source -> unit |
|
19 |
val begin_theory: string -> string list -> (Path.T * bool) list -> unit |
|
20 |
val end_theory: string -> unit |
|
21 |
val theorem: string -> thm -> unit |
|
22 |
end; |
|
23 |
||
24 |
structure BrowserInfo: BROWSER_INFO = |
|
25 |
struct |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
26 |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
27 |
|
6330 | 28 |
(** global browser info state **) |
29 |
||
30 |
(* type theory_info *) |
|
31 |
||
32 |
type theory_info = {source: Buffer.T, html: Buffer.T, graph: Buffer.T}; |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
33 |
|
6330 | 34 |
fun make_theory_info (source, html, graph) = |
35 |
{source = source, html = html, graph = graph}: theory_info; |
|
36 |
||
37 |
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty); |
|
38 |
fun map_theory_info f {source, html, graph} = make_theory_info (f (source, html, graph)); |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
39 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
40 |
|
6330 | 41 |
(* type browser_info *) |
42 |
||
43 |
type browser_info = {theories: theory_info Symtab.table, index: Buffer.T}; |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
44 |
|
6330 | 45 |
fun make_browser_info (theories, index) = |
46 |
{theories = theories, index = index}: browser_info; |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
47 |
|
6330 | 48 |
val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty); |
49 |
fun map_browser_info f {theories, index} = make_browser_info (f (theories, index)); |
|
50 |
||
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
51 |
|
6330 | 52 |
(* state *) |
53 |
||
54 |
val browser_info = ref empty_browser_info; |
|
55 |
||
56 |
fun change_browser_info f = browser_info := map_browser_info f (! browser_info); |
|
57 |
||
58 |
fun init_theory_info name info = change_browser_info (fn (theories, index) => |
|
59 |
(Symtab.update ((name, info), theories), index)); |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
60 |
|
6330 | 61 |
fun change_theory_info name f = change_browser_info (fn (theories, index) => |
62 |
(case Symtab.lookup (theories, name) of |
|
63 |
None => (warning ("Browser info: cannot access theory document " ^ quote name); |
|
64 |
(theories, index)) |
|
65 |
| Some info => (Symtab.update ((name, map_theory_info f info), theories), index))); |
|
66 |
||
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
67 |
|
6339 | 68 |
fun add_index txt = change_browser_info (fn (theories, index) => |
69 |
(theories, Buffer.add txt index)); |
|
70 |
||
6330 | 71 |
fun add_source name txt = change_theory_info name (fn (source, html, graph) => |
72 |
(Buffer.add txt source, html, graph)); |
|
73 |
||
74 |
fun add_html name txt = change_theory_info name (fn (source, html, graph) => |
|
75 |
(source, Buffer.add txt html, graph)); |
|
76 |
||
77 |
fun add_graph name txt = change_theory_info name (fn (source, html, graph) => |
|
78 |
(source, html, Buffer.add txt graph)); |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
79 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
80 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
81 |
|
6330 | 82 |
(** global session state **) |
83 |
||
84 |
(* paths *) |
|
85 |
||
86 |
val output_path = Path.variable "ISABELLE_BROWSER_INFO"; |
|
87 |
||
88 |
fun top_path sess_path = Path.append (Path.appends (replicate (length sess_path) Path.parent)); |
|
89 |
||
90 |
val html_ext = Path.ext "html"; |
|
91 |
val html_path = html_ext o Path.basic; |
|
92 |
val graph_path = Path.ext "graph" o Path.basic; |
|
93 |
val index_path = Path.basic "index.html"; |
|
94 |
||
6339 | 95 |
val session_path = Path.basic ".session"; |
96 |
val session_entries_path = Path.unpack ".session/entries"; |
|
97 |
val pre_index_path = Path.unpack ".session/pre-index"; |
|
98 |
||
6330 | 99 |
|
100 |
(* session_info *) |
|
101 |
||
102 |
type session_info = |
|
6342 | 103 |
{name: string, parent: string, session: string, path: string list, |
6330 | 104 |
html_prefix: Path.T, graph_prefix: Path.T}; |
105 |
||
6342 | 106 |
fun make_session_info (name, parent, session, path, html_prefix, graph_prefix) = |
107 |
{name = name, parent = parent, session = session, path = path, |
|
6330 | 108 |
html_prefix = html_prefix, graph_prefix = graph_prefix}: session_info; |
109 |
||
6348 | 110 |
|
111 |
(* state *) |
|
112 |
||
6330 | 113 |
val session_info = ref (None: session_info option); |
114 |
||
6348 | 115 |
fun with_session f = (case ! session_info of None => () | Some info => f info); |
116 |
fun with_context f = f (PureThy.get_name (Context.the_context ())); |
|
117 |
||
6330 | 118 |
|
119 |
||
6339 | 120 |
|
121 |
(** HTML output **) |
|
122 |
||
123 |
||
124 |
(* maintain index *) |
|
125 |
||
126 |
val session_entries = |
|
127 |
HTML.session_entries o map (fn name => (Path.append (Path.basic name) index_path, name)); |
|
128 |
||
129 |
fun get_entries dir = |
|
130 |
split_lines (File.read (Path.append dir session_entries_path)); |
|
131 |
||
132 |
fun put_entries entries dir = |
|
133 |
File.write (Path.append dir session_entries_path) (cat_lines entries); |
|
134 |
||
135 |
||
136 |
fun create_index dir = |
|
137 |
File.read (Path.append dir pre_index_path) ^ |
|
138 |
session_entries (get_entries dir) ^ HTML.end_index |
|
139 |
|> File.write (Path.append dir index_path); |
|
140 |
||
141 |
fun update_index dir name = |
|
142 |
(case try get_entries dir of |
|
6348 | 143 |
None => warning ("Browser info: cannot access session index in " ^ quote (Path.pack dir)) |
6339 | 144 |
| Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir)); |
6342 | 145 |
|
6339 | 146 |
|
6330 | 147 |
(* init session *) |
148 |
||
6342 | 149 |
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
6339 | 150 |
|
6348 | 151 |
fun could_copy inpath outpath = |
152 |
if File.exists inpath then (File.copy inpath outpath; true) |
|
153 |
else false; |
|
154 |
||
6342 | 155 |
fun init false _ _ = (browser_info := empty_browser_info; session_info := None) |
156 |
| init true path name = |
|
6330 | 157 |
let |
6348 | 158 |
val parent_name = name_of_session (take (length path - 1, path)); |
6342 | 159 |
val session_name = name_of_session path; |
6339 | 160 |
val sess_prefix = Path.make path; |
6330 | 161 |
val out_path = Path.expand output_path; |
162 |
val html_prefix = Path.append out_path sess_prefix; |
|
163 |
val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix]; |
|
6348 | 164 |
|
165 |
val _ = (File.mkdir html_prefix; File.mkdir graph_prefix); |
|
166 |
fun prep_readme readme = |
|
167 |
let val readme_path = Path.basic readme in |
|
168 |
if could_copy readme_path (Path.append html_prefix readme_path) then Some readme_path |
|
169 |
else None |
|
170 |
end; |
|
171 |
val opt_readme = |
|
172 |
(case prep_readme "README.html" of None => prep_readme "README" | some => some); |
|
173 |
val index_text = HTML.begin_index (Path.append Path.parent index_path, parent_name) |
|
174 |
(index_path, session_name) opt_readme; |
|
6330 | 175 |
in |
6339 | 176 |
File.mkdir (Path.append html_prefix session_path); |
177 |
File.write (Path.append html_prefix session_entries_path) ""; |
|
6342 | 178 |
session_info := Some (make_session_info (name, parent_name, session_name, path, |
6339 | 179 |
html_prefix, graph_prefix)); |
6330 | 180 |
browser_info := empty_browser_info; |
6348 | 181 |
add_index index_text |
6330 | 182 |
end; |
183 |
||
184 |
||
185 |
(* finish session *) |
|
186 |
||
6348 | 187 |
fun finish () = with_session (fn {name, html_prefix, graph_prefix, ...} => |
6339 | 188 |
let |
189 |
val {theories, index} = ! browser_info; |
|
6330 | 190 |
|
6339 | 191 |
fun finish_node (a, {source = _, html, graph}) = |
192 |
(Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html); |
|
193 |
Buffer.write (Path.append graph_prefix (graph_path a)) graph); |
|
194 |
in |
|
195 |
seq finish_node (Symtab.dest theories); |
|
196 |
Buffer.write (Path.append html_prefix pre_index_path) index; |
|
197 |
create_index html_prefix; |
|
198 |
update_index (Path.append html_prefix Path.parent) name; |
|
6330 | 199 |
browser_info := empty_browser_info; |
200 |
session_info := None |
|
201 |
end); |
|
202 |
||
203 |
||
6339 | 204 |
(* theory elements *) |
6330 | 205 |
|
6348 | 206 |
fun theory_source name src = with_session (fn _ => |
6330 | 207 |
(init_theory_info name empty_theory_info; add_source name (HTML.source src))); |
208 |
||
6339 | 209 |
|
210 |
(* FIXME clean *) |
|
211 |
||
6361 | 212 |
fun parent_link name = |
213 |
if is_some (Symtab.lookup (#theories (! browser_info), name)) then (Some (html_path name), name) |
|
214 |
else (None, name); |
|
215 |
||
216 |
fun begin_theory name raw_parents orig_files = with_session (fn {session, html_prefix, ...} => |
|
6330 | 217 |
let |
6361 | 218 |
val parents = map parent_link raw_parents; |
6330 | 219 |
val ml_path = ThyLoad.ml_path name; |
220 |
val files = orig_files @ (* FIXME improve!? *) |
|
221 |
(if is_some (ThyLoad.check_file ml_path) then [(ml_path, true)] else []); |
|
222 |
||
6348 | 223 |
fun prep_file (raw_path, loadit) = |
6330 | 224 |
(case ThyLoad.check_file raw_path of |
225 |
Some (path, _) => |
|
6348 | 226 |
let |
227 |
val base = Path.base path; |
|
228 |
val base_html = html_ext base; |
|
229 |
in |
|
230 |
File.write (Path.append html_prefix base_html) (HTML.ml_file base (File.read path)); |
|
231 |
(Some base_html, raw_path, loadit) |
|
6330 | 232 |
end |
6348 | 233 |
| None => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path)); |
234 |
(None, raw_path, loadit))); |
|
6330 | 235 |
|
6348 | 236 |
val files_html = map prep_file files; |
6330 | 237 |
fun prep_source (source, html, graph) = |
238 |
let val txt = |
|
239 |
HTML.begin_theory (index_path, session) name parents files_html (Buffer.content source) |
|
6348 | 240 |
in (Buffer.empty, Buffer.add txt html, graph) end; |
6330 | 241 |
in |
6339 | 242 |
change_theory_info name prep_source; |
243 |
add_index (HTML.theory_entry (html_path name, name)) |
|
6330 | 244 |
end); |
245 |
||
6339 | 246 |
fun end_theory _ = (); |
6330 | 247 |
|
6348 | 248 |
fun theorem name thm = with_session (fn _ => with_context add_html (HTML.theorem name thm)); |
249 |
fun section s = with_session (fn _ => with_context add_html (HTML.section s)); |
|
6330 | 250 |
|
251 |
||
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
252 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
253 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
254 |
|
6330 | 255 |
(* FIXME |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
256 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
257 |
(******************** Graph generation functions ************************) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
258 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
259 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
260 |
(*flag that indicates whether graph files should be generated*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
261 |
val make_graph = ref false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
262 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
263 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
264 |
(*file to use as basis for new graph files*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
265 |
val graph_base_file = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
266 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
267 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
268 |
(*directory containing basic theories (gets label "base")*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
269 |
val graph_root_dir = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
270 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
271 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
272 |
(*name of current graph file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
273 |
val graph_file = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
274 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
275 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
276 |
(*name of large graph file which also contains |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
277 |
theories defined in subdirectories *) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
278 |
val large_graph_file = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
279 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
280 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
281 |
(* initialize graph data generator *) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
282 |
fun init_graph usedir_arg = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
283 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
284 |
(*create default graph containing only Pure, CPure and ProtoPure*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
285 |
fun default_graph outfile = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
286 |
let val os = TextIO.openOut outfile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
287 |
in (TextIO.output(os,"\"ProtoPure\" \"ProtoPure\" \"Pure\" \"\" ;\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
288 |
\\"CPure\" \"CPure\" \"Pure\" \"\" > \"ProtoPure\" ;\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
289 |
\\"Pure\" \"Pure\" \"Pure\" \"\" > \"ProtoPure\" ;\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
290 |
TextIO.closeOut os) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
291 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
292 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
293 |
(*copy graph file, adjust relative paths for theory files*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
294 |
fun copy_graph infile outfile unfold = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
295 |
let val is = TextIO.openIn infile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
296 |
val (inp_dir, _) = split_filename infile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
297 |
val (outp_dir, _) = split_filename outfile; |
3834 | 298 |
val entries = map (BAD_space_explode " ") |
299 |
(BAD_space_explode "\n" (TextIO.inputAll is)); |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
300 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
301 |
fun thyfile f = if f = "\"\"" then f else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
302 |
let val (dir, name) = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
303 |
split_filename (implode (rev (tl (rev (tl (explode f)))))); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
304 |
val abs_path = normalize_path (tack_on inp_dir dir); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
305 |
val rel_path = tack_on (relative_path outp_dir abs_path) name |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
306 |
in quote rel_path end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
307 |
|
6330 | 308 |
fun process_entry (a::b::c::d::e::r) = |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
309 |
if d = "+" then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
310 |
a::b::c::((if unfold then "+ " else "") ^ (thyfile e))::r |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
311 |
else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
312 |
a::b::c::(thyfile d)::e::r; |
6330 | 313 |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
314 |
val _ = TextIO.closeIn is; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
315 |
val os = TextIO.openOut outfile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
316 |
val _ = TextIO.output(os, (cat_lines |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
317 |
(map ((space_implode " ") o process_entry) entries)) ^ "\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
318 |
val _ = TextIO.closeOut os; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
319 |
in () end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
320 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
321 |
(*create html page which contains graph browser applet*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
322 |
fun mk_applet_page abs_path large other_graph = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
323 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
324 |
val dir_name = |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
325 |
(if subdir_of (!original_path, !base_path) then "Isabelle/" else "") ^ |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
326 |
(relative_path (normalize_path (tack_on (!graph_root_dir) "..")) (pwd ())); |
6330 | 327 |
val rel_codebase = |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
328 |
relative_path abs_path (tack_on (normalize_path (!output_dir)) "graph"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
329 |
val rel_index_path = tack_on (relative_path |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
330 |
abs_path (tack_on (normalize_path (!output_dir)) "graph")) "index.html"; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
331 |
val outfile = |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
332 |
tack_on abs_path ((if large then "large" else "small") ^ ".html"); |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
333 |
val os = TextIO.openOut outfile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
334 |
val _ = TextIO.output(os, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
335 |
"<HTML><HEAD><TITLE>" ^ dir_name ^ "</TITLE></HEAD>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
336 |
\<BODY><H2>" ^ dir_name ^ "</H2>\n" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
337 |
(if other_graph then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
338 |
(if large then |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
339 |
"View <A HREF=\"small.html\">small graph</A> without \ |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
340 |
\subdirectories<P>\n" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
341 |
else |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
342 |
"View <A HREF=\"large.html\">large graph</A> including \ |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
343 |
\all subdirectories<P>\n") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
344 |
else "") ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
345 |
"<A HREF=\"" ^ rel_index_path ^ "\">Back</A> to index\n<HR>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
346 |
\<APPLET CODE=\"GraphBrowser/GraphBrowser.class\" \ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
347 |
\CODEBASE=\"" ^ rel_codebase ^ "\" WIDTH=550 HEIGHT=450>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
348 |
\<PARAM NAME=\"graphfile\" VALUE=\"" ^ |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
349 |
(if large then "large.graph" else "small.graph") ^ "\">\n\ |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
350 |
\</APPLET>\n<HR>\n</BODY></HTML>") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
351 |
val _ = TextIO.closeOut os |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
352 |
in () end; |
6330 | 353 |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
354 |
val gpath = graph_path (pwd ()); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
355 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
356 |
in |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
357 |
(make_graph := true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
358 |
base_path := normalize_path (!base_path); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
359 |
mkdir gpath; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
360 |
original_path := pwd (); |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
361 |
graph_file := tack_on gpath "small.graph"; |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
362 |
graph_root_dir := (if usedir_arg = "." then pwd () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
363 |
else normalize_path (tack_on (pwd ()) "..")); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
364 |
(if (!graph_base_file) = "" then |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
365 |
(large_graph_file := tack_on gpath "large.graph"; |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
366 |
default_graph (!graph_file); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
367 |
default_graph (!large_graph_file); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
368 |
mk_applet_page gpath false true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
369 |
mk_applet_page gpath true true) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
370 |
else |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
371 |
(if subdir_of (fst (split_filename (!graph_file)), |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
372 |
(fst (split_filename (!graph_base_file)))) |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
373 |
then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
374 |
(copy_graph (!graph_base_file) (!graph_file) true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
375 |
mk_applet_page gpath false false) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
376 |
else |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
377 |
(large_graph_file := tack_on gpath "large.graph"; |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
378 |
mk_applet_page gpath false true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
379 |
mk_applet_page gpath true true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
380 |
copy_graph (!graph_base_file) (!graph_file) false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
381 |
copy_graph (!graph_base_file) (!large_graph_file) false))); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
382 |
graph_base_file := (!graph_file)) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
383 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
384 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
385 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
386 |
(*add theory to graph definition file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
387 |
fun mk_graph tname abs_path = if not (!make_graph) then () else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
388 |
let val parents = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
389 |
map (fn (t, _) => tack_on (path_of t) t) |
3976 | 390 |
(filter (fn (_, {children,...}) => tname mem children) |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
391 |
(Symtab.dest(!loaded_thys))); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
392 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
393 |
val dir_name = relative_path |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
394 |
(normalize_path (tack_on (!graph_root_dir) "..")) abs_path; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
395 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
396 |
val dir_entry = "\"" ^ dir_name ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
397 |
(if (tack_on abs_path "") = (tack_on (!graph_root_dir) "") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
398 |
then "/base\" + " else "\" "); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
399 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
400 |
val thy_file = (tack_on (html_path abs_path) tname) ^ ".html"; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
401 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
402 |
val thy_ID = quote (tack_on abs_path tname); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
403 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
404 |
val entry_str_1 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
405 |
(quote (relative_path (fst (split_filename (!graph_file))) thy_file)) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
406 |
" > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
407 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
408 |
val entry_str_2 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
409 |
(quote (relative_path (fst (split_filename (!large_graph_file))) thy_file)) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
410 |
" > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
411 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
412 |
fun exists_entry id infile = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
413 |
let val is = TextIO.openIn(infile); |
3834 | 414 |
val IDs = map (hd o tl o (BAD_space_explode " ")) |
415 |
(BAD_space_explode "\n" (TextIO.inputAll is)); |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
416 |
val _ = TextIO.closeIn is |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
417 |
in id mem IDs end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
418 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
419 |
fun mk_entry outfile entry_str = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
420 |
if exists_entry thy_ID outfile then () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
421 |
else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
422 |
let val os = TextIO.openAppend outfile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
423 |
val _ = TextIO.output (os, entry_str); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
424 |
val _ = TextIO.closeOut os; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
425 |
in () end |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
426 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
427 |
in (mk_entry (!graph_file) entry_str_1; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
428 |
mk_entry (!large_graph_file) entry_str_2) handle _ => |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
429 |
(make_graph:=false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
430 |
warning ("Unable to write to graph file " ^ (!graph_file))) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
431 |
end; |
6342 | 432 |
|
6330 | 433 |
*) |