author | wenzelm |
Wed, 22 Sep 1999 20:57:51 +0200 | |
changeset 7572 | 6e6dafacbc28 |
parent 7409 | f8ce7b832598 |
child 7634 | c326808da921 |
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 |
|
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
16 |
val init: bool -> string list -> string -> Url.T option * bool -> unit |
6330 | 17 |
val finish: unit -> unit |
18 |
val theory_source: string -> (string, 'a) Source.source -> unit |
|
6649 | 19 |
val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory |
6330 | 20 |
val end_theory: string -> unit |
7572 | 21 |
val result: string -> string -> thm -> unit |
22 |
val results: string -> string -> thm list -> unit |
|
6330 | 23 |
val theorem: string -> thm -> unit |
7409 | 24 |
val theorems: string -> thm list -> unit |
6649 | 25 |
val setup: (theory -> theory) list |
6330 | 26 |
end; |
27 |
||
28 |
structure BrowserInfo: BROWSER_INFO = |
|
29 |
struct |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
30 |
|
6665 | 31 |
|
6649 | 32 |
(** paths **) |
6330 | 33 |
|
34 |
val output_path = Path.variable "ISABELLE_BROWSER_INFO"; |
|
35 |
||
7572 | 36 |
fun top_path sess_path offset = |
37 |
Path.append (Path.appends (replicate (offset + length sess_path) Path.parent)); |
|
6330 | 38 |
|
39 |
val html_ext = Path.ext "html"; |
|
40 |
val html_path = html_ext o Path.basic; |
|
41 |
val graph_path = Path.ext "graph" o Path.basic; |
|
42 |
val index_path = Path.basic "index.html"; |
|
43 |
||
6339 | 44 |
val session_path = Path.basic ".session"; |
45 |
val session_entries_path = Path.unpack ".session/entries"; |
|
46 |
val pre_index_path = Path.unpack ".session/pre-index"; |
|
47 |
||
6330 | 48 |
|
6665 | 49 |
|
6649 | 50 |
(** additional theory data **) |
51 |
||
52 |
structure BrowserInfoArgs = |
|
53 |
struct |
|
54 |
val name = "Pure/browser_info"; |
|
55 |
type T = {session: string list, is_local: bool}; |
|
56 |
||
57 |
val empty = {session = [], is_local = false}; |
|
58 |
val copy = I; |
|
59 |
val prep_ext = I; |
|
60 |
fun merge _ = empty; |
|
61 |
fun print _ _ = (); |
|
62 |
end; |
|
63 |
||
64 |
structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs); |
|
6665 | 65 |
|
66 |
fun get_info thy = |
|
67 |
if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty |
|
68 |
else BrowserInfoData.get thy; |
|
69 |
||
70 |
||
6649 | 71 |
|
72 |
(** graphs **) |
|
73 |
||
74 |
type graph_node = |
|
75 |
{name: string, ID: string, dir: string, unfold: bool, |
|
76 |
path: string, parents: string list}; |
|
77 |
||
78 |
fun get_graph path = map (fn (a :: b :: c :: d :: e :: r) => |
|
79 |
{name = unenclose a, ID = unenclose b, |
|
80 |
dir = unenclose c, unfold = (d = "+"), |
|
81 |
path = unenclose (if d = "+" then e else d), |
|
82 |
parents = map unenclose (fst (split_last (if d = "+" then tl r else r)))}) |
|
83 |
(map (filter_out (equal "") o space_explode " ") (split_lines (File.read path))); |
|
84 |
||
85 |
fun put_graph gr path = File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => |
|
86 |
"\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
|
87 |
path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); |
|
88 |
||
89 |
fun dir_of sess = space_implode "/" (case sess of |
|
90 |
[] => ["Pure"] | [x] => [x, "base"] | xs => xs); |
|
91 |
||
92 |
fun ID_of sess s = dir_of sess ^ "/" ^ s; |
|
93 |
||
94 |
(* retrieve graph data from theory loader database *) |
|
95 |
||
96 |
fun make_graph remote_path unfold curr_sess = map (fn name => |
|
97 |
let |
|
98 |
val {session, is_local} = get_info (ThyInfo.theory name); |
|
99 |
val path' = Path.append (Path.make session) (html_path name) |
|
100 |
in |
|
101 |
{name = name, ID = ID_of session name, dir = dir_of session, |
|
102 |
path = if null session then "" else |
|
103 |
if is_some remote_path andalso not is_local then |
|
104 |
Url.pack (Url.append (the remote_path) (Url.file path')) |
|
105 |
else Path.pack (top_path curr_sess 2 path'), |
|
106 |
unfold = unfold andalso (length session = 1), |
|
107 |
parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) |
|
108 |
(ThyInfo.get_preds name)} |
|
109 |
end) (ThyInfo.names ()); |
|
110 |
||
111 |
fun add_graph_entry' (entry as {ID, ...}) (gr : graph_node list) = |
|
112 |
filter_out (fn entry' => #ID entry' = ID) gr @ [entry]; |
|
113 |
||
114 |
||
6665 | 115 |
|
6649 | 116 |
(** global browser info state **) |
117 |
||
118 |
(* type theory_info *) |
|
119 |
||
120 |
type theory_info = {source: Buffer.T, html: Buffer.T}; |
|
121 |
||
122 |
fun make_theory_info (source, html) = |
|
123 |
{source = source, html = html}: theory_info; |
|
124 |
||
125 |
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty); |
|
126 |
fun map_theory_info f {source, html} = make_theory_info (f (source, html)); |
|
127 |
||
128 |
||
129 |
(* type browser_info *) |
|
130 |
||
131 |
type browser_info = {theories: theory_info Symtab.table, index: Buffer.T, |
|
132 |
graph: graph_node list, all_graph: graph_node list}; |
|
133 |
||
134 |
fun make_browser_info (theories, index, graph, all_graph) = |
|
135 |
{theories = theories, index = index, graph = graph, all_graph = all_graph}: browser_info; |
|
136 |
||
137 |
val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty, [], []); |
|
138 |
||
139 |
fun initial_browser_info remote_path graph_path curr_sess = make_browser_info |
|
140 |
(Symtab.empty, Buffer.empty, make_graph remote_path false curr_sess, |
|
141 |
if_none (try get_graph graph_path) (make_graph remote_path true [""])); |
|
142 |
||
143 |
fun map_browser_info f {theories, index, graph, all_graph} = |
|
144 |
make_browser_info (f (theories, index, graph, all_graph)); |
|
145 |
||
146 |
||
147 |
(* state *) |
|
148 |
||
149 |
val browser_info = ref empty_browser_info; |
|
150 |
||
151 |
fun change_browser_info f = browser_info := map_browser_info f (! browser_info); |
|
152 |
||
153 |
fun init_theory_info name info = change_browser_info (fn (theories, index, graph, all_graph) => |
|
154 |
(Symtab.update ((name, info), theories), index, graph, all_graph)); |
|
155 |
||
156 |
fun change_theory_info name f = change_browser_info (fn (theories, index, graph, all_graph) => |
|
157 |
(case Symtab.lookup (theories, name) of |
|
158 |
None => (warning ("Browser info: cannot access theory document " ^ quote name); |
|
159 |
(theories, index, graph, all_graph)) |
|
160 |
| Some info => (Symtab.update ((name, map_theory_info f info), theories), index, graph, all_graph))); |
|
161 |
||
162 |
||
163 |
fun add_index txt = change_browser_info (fn (theories, index, graph, all_graph) => |
|
164 |
(theories, Buffer.add txt index, graph, all_graph)); |
|
165 |
||
6665 | 166 |
(*add entry to graph for current session*) |
6649 | 167 |
fun add_graph_entry e = change_browser_info (fn (theories, index, graph, all_graph) => |
168 |
(theories, index, add_graph_entry' e graph, all_graph)); |
|
169 |
||
6665 | 170 |
(*add entry to graph for all sessions*) |
6649 | 171 |
fun add_all_graph_entry e = change_browser_info (fn (theories, index, graph, all_graph) => |
172 |
(theories, index, graph, add_graph_entry' e all_graph)); |
|
173 |
||
174 |
fun add_source name txt = change_theory_info name (fn (source, html) => |
|
175 |
(Buffer.add txt source, html)); |
|
176 |
||
177 |
fun add_html name txt = change_theory_info name (fn (source, html) => |
|
178 |
(source, Buffer.add txt html)); |
|
179 |
||
180 |
||
6665 | 181 |
|
6649 | 182 |
(** global session state **) |
183 |
||
6330 | 184 |
(* session_info *) |
185 |
||
186 |
type session_info = |
|
6342 | 187 |
{name: string, parent: string, session: string, path: string list, |
6649 | 188 |
html_prefix: Path.T, graph_path: Path.T, all_graph_path: Path.T, remote_path: Url.T option}; |
6330 | 189 |
|
6649 | 190 |
fun make_session_info (name, parent, session, path, html_prefix, graph_path, all_graph_path, remote_path) = |
6342 | 191 |
{name = name, parent = parent, session = session, path = path, |
6649 | 192 |
html_prefix = html_prefix, graph_path = graph_path, |
193 |
all_graph_path = all_graph_path, remote_path = remote_path}: session_info; |
|
6330 | 194 |
|
6348 | 195 |
|
196 |
(* state *) |
|
197 |
||
6330 | 198 |
val session_info = ref (None: session_info option); |
199 |
||
6649 | 200 |
fun with_session x f = (case ! session_info of None => x | Some info => f info); |
6348 | 201 |
fun with_context f = f (PureThy.get_name (Context.the_context ())); |
202 |
||
6330 | 203 |
|
6665 | 204 |
|
6339 | 205 |
(** HTML output **) |
206 |
||
207 |
(* maintain index *) |
|
208 |
||
209 |
val session_entries = |
|
6649 | 210 |
HTML.session_entries o map (fn name => (Url.file (Path.append (Path.basic name) index_path), name)); |
6339 | 211 |
|
212 |
fun get_entries dir = |
|
213 |
split_lines (File.read (Path.append dir session_entries_path)); |
|
214 |
||
215 |
fun put_entries entries dir = |
|
216 |
File.write (Path.append dir session_entries_path) (cat_lines entries); |
|
217 |
||
218 |
||
219 |
fun create_index dir = |
|
220 |
File.read (Path.append dir pre_index_path) ^ |
|
221 |
session_entries (get_entries dir) ^ HTML.end_index |
|
222 |
|> File.write (Path.append dir index_path); |
|
223 |
||
224 |
fun update_index dir name = |
|
225 |
(case try get_entries dir of |
|
6388 | 226 |
None => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir)) |
6339 | 227 |
| Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir)); |
6342 | 228 |
|
6339 | 229 |
|
6330 | 230 |
(* init session *) |
231 |
||
6342 | 232 |
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
6339 | 233 |
|
6348 | 234 |
fun could_copy inpath outpath = |
235 |
if File.exists inpath then (File.copy inpath outpath; true) |
|
236 |
else false; |
|
237 |
||
6649 | 238 |
fun init false _ _ _ = (browser_info := empty_browser_info; session_info := None) |
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
239 |
| init true path name (remote_path, first_time) = |
6330 | 240 |
let |
6348 | 241 |
val parent_name = name_of_session (take (length path - 1, path)); |
6342 | 242 |
val session_name = name_of_session path; |
6339 | 243 |
val sess_prefix = Path.make path; |
6330 | 244 |
val out_path = Path.expand output_path; |
245 |
val html_prefix = Path.append out_path sess_prefix; |
|
246 |
val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix]; |
|
6649 | 247 |
val graph_path = Path.append graph_prefix (Path.basic "session.graph"); |
248 |
val graph_lnk = Url.file (top_path path 0 (Path.appends |
|
249 |
[Path.unpack "graph/data", sess_prefix, Path.basic "medium.html"])); |
|
250 |
val graph_up_lnk = (Url.file (top_path path 2 (Path.append sess_prefix index_path)), session_name); |
|
251 |
val codebase = Url.file (top_path path 1 Path.current); |
|
252 |
val all_graph_path = Path.appends [out_path, Path.unpack "graph/data", |
|
253 |
Path.basic (hd path), Path.basic "all_sessions.graph"]; |
|
6348 | 254 |
|
255 |
val _ = (File.mkdir html_prefix; File.mkdir graph_prefix); |
|
256 |
fun prep_readme readme = |
|
257 |
let val readme_path = Path.basic readme in |
|
258 |
if could_copy readme_path (Path.append html_prefix readme_path) then Some readme_path |
|
259 |
else None |
|
260 |
end; |
|
261 |
val opt_readme = |
|
262 |
(case prep_readme "README.html" of None => prep_readme "README" | some => some); |
|
7236
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
263 |
|
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
264 |
val parent_index_path = Path.append Path.parent index_path; |
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
265 |
val index_up_lnk = if first_time then |
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
266 |
Url.append (the remote_path) (Url.file (Path.append sess_prefix parent_index_path)) |
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
267 |
else Url.file parent_index_path; |
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
268 |
|
e077484d50d8
Better handling of path for remote theory browsing information.
berghofe
parents:
6665
diff
changeset
|
269 |
val index_text = HTML.begin_index (index_up_lnk, parent_name) |
6649 | 270 |
(Url.file index_path, session_name) (apsome Url.file opt_readme) graph_lnk; |
6330 | 271 |
in |
6339 | 272 |
File.mkdir (Path.append html_prefix session_path); |
273 |
File.write (Path.append html_prefix session_entries_path) ""; |
|
6649 | 274 |
seq (fn (name, txt) => File.write (Path.append graph_prefix (Path.basic name)) txt) |
275 |
(HTML.applet_pages session_name codebase graph_up_lnk (length path = 1)); |
|
6342 | 276 |
session_info := Some (make_session_info (name, parent_name, session_name, path, |
6649 | 277 |
html_prefix, graph_path, all_graph_path, remote_path)); |
278 |
browser_info := initial_browser_info remote_path all_graph_path path; |
|
6348 | 279 |
add_index index_text |
6330 | 280 |
end; |
281 |
||
282 |
||
283 |
(* finish session *) |
|
284 |
||
6649 | 285 |
fun finish () = with_session () (fn {name, html_prefix, graph_path, all_graph_path, path, ...} => |
6339 | 286 |
let |
6649 | 287 |
val {theories, index, graph, all_graph} = ! browser_info; |
6330 | 288 |
|
6649 | 289 |
fun finish_node (a, {source = _, html}) = |
290 |
Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html); |
|
6339 | 291 |
in |
292 |
seq finish_node (Symtab.dest theories); |
|
293 |
Buffer.write (Path.append html_prefix pre_index_path) index; |
|
6649 | 294 |
put_graph graph graph_path; |
295 |
put_graph all_graph all_graph_path; |
|
6339 | 296 |
create_index html_prefix; |
297 |
update_index (Path.append html_prefix Path.parent) name; |
|
6330 | 298 |
browser_info := empty_browser_info; |
299 |
session_info := None |
|
300 |
end); |
|
301 |
||
302 |
||
6339 | 303 |
(* theory elements *) |
6330 | 304 |
|
6649 | 305 |
fun theory_source name src = with_session () (fn _ => |
6330 | 306 |
(init_theory_info name empty_theory_info; add_source name (HTML.source src))); |
307 |
||
6339 | 308 |
|
309 |
(* FIXME clean *) |
|
310 |
||
6649 | 311 |
fun parent_link remote_path curr_session name = |
312 |
let |
|
313 |
val {session, is_local} = get_info (ThyInfo.theory name); |
|
314 |
val path = Path.append (Path.make session) (html_path name) |
|
315 |
in (if null session then None else |
|
316 |
Some (if is_some remote_path andalso not is_local then |
|
317 |
Url.append (the remote_path) (Url.file path) |
|
318 |
else Url.file (top_path curr_session 0 path)), name) |
|
319 |
end; |
|
6361 | 320 |
|
6649 | 321 |
fun begin_theory name raw_parents orig_files thy = |
322 |
with_session thy (fn {session, path, html_prefix, remote_path, ...} => |
|
6330 | 323 |
let |
6649 | 324 |
val parents = map (parent_link remote_path path) raw_parents; |
6330 | 325 |
val ml_path = ThyLoad.ml_path name; |
7409 | 326 |
val files = map (apsnd Some) orig_files @ |
327 |
(if is_some (ThyLoad.check_file ml_path) then [(ml_path, None)] else []); |
|
6330 | 328 |
|
6348 | 329 |
fun prep_file (raw_path, loadit) = |
6330 | 330 |
(case ThyLoad.check_file raw_path of |
331 |
Some (path, _) => |
|
6348 | 332 |
let |
333 |
val base = Path.base path; |
|
334 |
val base_html = html_ext base; |
|
335 |
in |
|
6649 | 336 |
File.write (Path.append html_prefix base_html) (HTML.ml_file (Url.file base) (File.read path)); |
337 |
(Some (Url.file base_html), Url.file raw_path, loadit) |
|
6330 | 338 |
end |
6348 | 339 |
| None => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path)); |
6649 | 340 |
(None, Url.file raw_path, loadit))); |
6330 | 341 |
|
6348 | 342 |
val files_html = map prep_file files; |
6649 | 343 |
|
344 |
fun prep_source (source, html) = |
|
6330 | 345 |
let val txt = |
6649 | 346 |
HTML.begin_theory (Url.file index_path, session) name parents files_html (Buffer.content source) |
347 |
in (Buffer.empty, Buffer.add txt html) end; |
|
348 |
||
349 |
fun make_entry unfold all = |
|
350 |
{name = name, ID = ID_of path name, dir = dir_of path, unfold = unfold, |
|
351 |
path = Path.pack (top_path (if all then [""] else path) 2 |
|
352 |
(Path.append (Path.make path) (html_path name))), |
|
353 |
parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents}; |
|
354 |
||
6330 | 355 |
in |
6339 | 356 |
change_theory_info name prep_source; |
6649 | 357 |
add_all_graph_entry (make_entry (length path = 1) true); |
358 |
add_graph_entry (make_entry true false); |
|
359 |
add_index (HTML.theory_entry (Url.file (html_path name), name)); |
|
360 |
BrowserInfoData.put {session = path, is_local = is_some remote_path} thy |
|
6330 | 361 |
end); |
362 |
||
6339 | 363 |
fun end_theory _ = (); |
6330 | 364 |
|
7572 | 365 |
fun result k a thm = with_session () (fn _ => with_context add_html (HTML.result k a thm)); |
366 |
fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms)); |
|
367 |
fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm)); |
|
368 |
fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms)); |
|
6649 | 369 |
fun section s = with_session () (fn _ => with_context add_html (HTML.section s)); |
6330 | 370 |
|
371 |
||
6665 | 372 |
|
373 |
(** theory setup **) |
|
374 |
||
375 |
val setup = [BrowserInfoData.init]; |
|
376 |
||
377 |
||
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
378 |
end; |