18 val write_graph: {name: string, ID: string, dir: string, unfold: bool, |
18 val write_graph: {name: string, ID: string, dir: string, unfold: bool, |
19 path: string, parents: string list} list -> Path.T -> unit |
19 path: string, parents: string list} list -> Path.T -> unit |
20 val display_graph: {name: string, ID: string, dir: string, unfold: bool, |
20 val display_graph: {name: string, ID: string, dir: string, unfold: bool, |
21 path: string, parents: string list} list -> unit |
21 path: string, parents: string list} list -> unit |
22 val init: bool -> bool -> string -> bool -> string list -> string list -> |
22 val init: bool -> bool -> string -> bool -> string list -> string list -> |
23 string -> (bool * Path.T) option -> Url.T option * bool -> bool -> unit |
23 string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit |
24 val finish: unit -> unit |
24 val finish: unit -> unit |
25 val init_theory: string -> unit |
25 val init_theory: string -> unit |
26 val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit |
26 val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit |
27 val theory_output: string -> string -> unit |
27 val theory_output: string -> string -> unit |
28 val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory -> theory |
28 val begin_theory: Path.T -> (Path.T * bool) list -> theory -> theory |
29 val add_hook: (string -> (string * thm list) list -> unit) -> unit |
29 val add_hook: (string -> (string * thm list) list -> unit) -> unit |
30 val results: string -> (string * thm list) list -> unit |
30 val results: string -> (string * thm list) list -> unit |
31 val theorem: string -> thm -> unit |
31 val theorem: string -> thm -> unit |
32 val theorems: string -> thm list -> unit |
32 val theorems: string -> thm list -> unit |
33 val chapter: string -> unit |
33 val chapter: string -> unit |
108 val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &"); |
108 val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &"); |
109 in () end; |
109 in () end; |
110 |
110 |
111 |
111 |
112 fun ID_of sess s = space_implode "/" (sess @ [s]); |
112 fun ID_of sess s = space_implode "/" (sess @ [s]); |
113 |
113 fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy); |
114 (*retrieve graph data from initial theory loader database*) |
114 |
115 fun init_graph remote_path curr_sess = map (fn name => |
115 |
116 let |
116 (*retrieve graph data from initial collection of theories*) |
117 val {name = sess_name, session, is_local} = get_info (ThyInfo.theory name); |
117 fun init_graph remote_path curr_sess = map (fn thy => |
|
118 let |
|
119 val name = Context.theory_name thy; |
|
120 val {name = sess_name, session, is_local} = get_info thy; |
118 val path' = Path.append (Path.make session) (html_path name); |
121 val path' = Path.append (Path.make session) (html_path name); |
119 in |
122 in |
120 {name = name, ID = ID_of session name, dir = sess_name, |
123 {name = name, ID = ID_of session name, dir = sess_name, |
121 path = |
124 path = |
122 if null session then "" else |
125 if null session then "" else |
123 if is_some remote_path andalso not is_local then |
126 if is_some remote_path andalso not is_local then |
124 Url.implode (Url.append (the remote_path) (Url.File |
127 Url.implode (Url.append (the remote_path) (Url.File |
125 (Path.append (Path.make session) (html_path name)))) |
128 (Path.append (Path.make session) (html_path name)))) |
126 else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)), |
129 else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)), |
127 unfold = false, |
130 unfold = false, |
128 parents = |
131 parents = map ID_of_thy (Theory.parents_of thy)} |
129 map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_parents name)} |
132 end); |
130 end) (ThyInfo.names ()); |
|
131 |
133 |
132 fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) = |
134 fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) = |
133 filter_out (fn entry' => #ID entry' = ID) gr @ [entry]; |
135 filter_out (fn entry' => #ID entry' = ID) gr @ [entry]; |
134 |
136 |
135 |
137 |
158 {theories = theories, files = files, tex_index = tex_index, html_index = html_index, |
160 {theories = theories, files = files, tex_index = tex_index, html_index = html_index, |
159 graph = graph}: browser_info; |
161 graph = graph}: browser_info; |
160 |
162 |
161 val empty_browser_info = make_browser_info (Symtab.empty, [], Buffer.empty, Buffer.empty, []); |
163 val empty_browser_info = make_browser_info (Symtab.empty, [], Buffer.empty, Buffer.empty, []); |
162 |
164 |
163 fun init_browser_info remote_path curr_sess = make_browser_info |
165 fun init_browser_info remote_path curr_sess thys = make_browser_info |
164 (Symtab.empty, [], Buffer.empty, Buffer.empty, init_graph remote_path curr_sess); |
166 (Symtab.empty, [], Buffer.empty, Buffer.empty, init_graph remote_path curr_sess thys); |
165 |
167 |
166 fun map_browser_info f {theories, files, tex_index, html_index, graph} = |
168 fun map_browser_info f {theories, files, tex_index, html_index, graph} = |
167 make_browser_info (f (theories, files, tex_index, html_index, graph)); |
169 make_browser_info (f (theories, files, tex_index, html_index, graph)); |
168 |
170 |
169 |
171 |
286 (* init session *) |
288 (* init session *) |
287 |
289 |
288 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
290 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
289 |
291 |
290 fun init build info doc doc_graph doc_versions path name doc_prefix2 |
292 fun init build info doc doc_graph doc_versions path name doc_prefix2 |
291 (remote_path, first_time) verbose = |
293 (remote_path, first_time) verbose thys = |
292 if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then |
294 if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then |
293 (browser_info := empty_browser_info; session_info := NONE) |
295 (browser_info := empty_browser_info; session_info := NONE) |
294 else |
296 else |
295 let |
297 let |
296 val parent_name = name_of_session (Library.take (length path - 1, path)); |
298 val parent_name = name_of_session (Library.take (length path - 1, path)); |
321 val index_text = HTML.begin_index (index_up_lnk, parent_name) |
323 val index_text = HTML.begin_index (index_up_lnk, parent_name) |
322 (Url.File index_path, session_name) docs (Url.explode "medium.html"); |
324 (Url.File index_path, session_name) docs (Url.explode "medium.html"); |
323 in |
325 in |
324 session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix, |
326 session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix, |
325 info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme)); |
327 info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme)); |
326 browser_info := init_browser_info remote_path path; |
328 browser_info := init_browser_info remote_path path thys; |
327 add_html_index index_text |
329 add_html_index index_text |
328 end; |
330 end; |
329 |
331 |
330 |
332 |
331 (* isatool wrappers *) |
333 (* isatool wrappers *) |
439 |
441 |
440 fun theory_output name s = |
442 fun theory_output name s = |
441 with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s)); |
443 with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s)); |
442 |
444 |
443 |
445 |
444 fun parent_link remote_path curr_session name = |
446 fun parent_link remote_path curr_session thy = |
445 let val {name = _, session, is_local} = get_info (ThyInfo.theory name) |
447 let |
446 in (if null session then NONE else |
448 val {name = _, session, is_local} = get_info thy; |
447 SOME (if is_some remote_path andalso not is_local then |
449 val name = Context.theory_name thy; |
448 Url.append (the remote_path) (Url.File |
450 val link = |
449 (Path.append (Path.make session) (html_path name))) |
451 if null session then NONE |
450 else Url.File (Path.append (mk_rel_path curr_session session) |
452 else SOME |
451 (html_path name))), name) |
453 (if is_some remote_path andalso not is_local then |
452 end; |
454 Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name))) |
453 |
455 else Url.File (Path.append (mk_rel_path curr_session session) (html_path name))); |
454 fun begin_theory dir name raw_parents orig_files thy = |
456 in (link, name) end; |
|
457 |
|
458 fun begin_theory dir orig_files thy = |
455 with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => |
459 with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => |
456 let |
460 let |
457 val parents = map (parent_link remote_path path) raw_parents; |
461 val name = Context.theory_name thy; |
|
462 val parents = Theory.parents_of thy; |
|
463 val parent_specs = map (parent_link remote_path path) parents; |
458 val ml_path = ThyLoad.ml_path name; |
464 val ml_path = ThyLoad.ml_path name; |
459 val files = map (apsnd SOME) orig_files @ |
465 val files = map (apsnd SOME) orig_files @ |
460 (if is_some (ThyLoad.check_file dir ml_path) then [(ml_path, NONE)] else []); |
466 (if is_some (ThyLoad.check_file dir ml_path) then [(ml_path, NONE)] else []); |
461 |
467 |
462 fun prep_file (raw_path, loadit) = |
468 fun prep_file (raw_path, loadit) = |
477 val files_html = map prep_file files; |
483 val files_html = map prep_file files; |
478 |
484 |
479 fun prep_html_source (tex_source, html_source, html) = |
485 fun prep_html_source (tex_source, html_source, html) = |
480 let |
486 let |
481 val txt = HTML.begin_theory (Url.File index_path, session) |
487 val txt = HTML.begin_theory (Url.File index_path, session) |
482 name parents files_html (Buffer.content html_source) |
488 name parent_specs files_html (Buffer.content html_source) |
483 in (tex_source, Buffer.empty, Buffer.add txt html) end; |
489 in (tex_source, Buffer.empty, Buffer.add txt html) end; |
484 |
490 |
485 val entry = |
491 val entry = |
486 {name = name, ID = ID_of path name, dir = sess_name, unfold = true, |
492 {name = name, ID = ID_of path name, dir = sess_name, unfold = true, |
487 path = Path.implode (html_path name), |
493 path = Path.implode (html_path name), |
488 parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents}; |
494 parents = map ID_of_thy parents}; |
489 |
495 |
490 in |
496 in |
491 change_theory_info name prep_html_source; |
497 change_theory_info name prep_html_source; |
492 add_graph_entry entry; |
498 add_graph_entry entry; |
493 add_html_index (HTML.theory_entry (Url.File (html_path name), name)); |
499 add_html_index (HTML.theory_entry (Url.File (html_path name), name)); |