21 path: string, parents: string list} list -> unit |
20 path: string, parents: string list} list -> unit |
22 val init: bool -> bool -> string -> bool -> string list -> string list -> |
21 val init: bool -> bool -> string -> bool -> string list -> string list -> |
23 string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit |
22 string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit |
24 val finish: unit -> unit |
23 val finish: unit -> unit |
25 val init_theory: string -> unit |
24 val init_theory: string -> unit |
26 val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit |
25 val theory_source: string -> (unit -> HTML.text) -> unit |
27 val theory_output: string -> string -> unit |
26 val theory_output: string -> string -> unit |
28 val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory |
27 val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory |
29 val add_hook: (string -> (string * thm list) list -> unit) -> unit |
|
30 val results: string -> (string * thm list) list -> unit |
|
31 val theorem: string -> thm -> unit |
|
32 val theorems: string -> thm list -> unit |
|
33 val chapter: string -> unit |
|
34 val subsection: string -> unit |
|
35 val subsubsection: string -> unit |
|
36 val drafts: string -> Path.T list -> Path.T |
28 val drafts: string -> Path.T list -> Path.T |
37 end; |
29 end; |
38 |
30 |
39 structure Present: PRESENT = |
31 structure Present: PRESENT = |
40 struct |
32 struct |
260 File.write (Path.append dir session_entries_path) (cat_lines entries); |
252 File.write (Path.append dir session_entries_path) (cat_lines entries); |
261 |
253 |
262 |
254 |
263 fun create_index dir = |
255 fun create_index dir = |
264 File.read (Path.append dir pre_index_path) ^ |
256 File.read (Path.append dir pre_index_path) ^ |
265 session_entries (get_entries dir) ^ HTML.end_index |
257 session_entries (get_entries dir) ^ HTML.end_document |
266 |> File.write (Path.append dir index_path); |
258 |> File.write (Path.append dir index_path); |
267 |
259 |
268 fun update_index dir name = CRITICAL (fn () => |
260 fun update_index dir name = CRITICAL (fn () => |
269 (case try get_entries dir of |
261 (case try get_entries dir of |
270 NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir)) |
262 NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir)) |
381 val thys = Symtab.dest theories; |
373 val thys = Symtab.dest theories; |
382 val parent_html_prefix = Path.append html_prefix Path.parent; |
374 val parent_html_prefix = Path.append html_prefix Path.parent; |
383 |
375 |
384 fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path; |
376 fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path; |
385 fun finish_html (a, {html, ...}: theory_info) = |
377 fun finish_html (a, {html, ...}: theory_info) = |
386 Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html); |
378 Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html); |
387 |
379 |
388 val sorted_graph = sorted_index graph; |
380 val sorted_graph = sorted_index graph; |
389 val opt_graphs = |
381 val opt_graphs = |
390 if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then |
382 if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then |
391 SOME (isatool_browser sorted_graph) |
383 SOME (isatool_browser sorted_graph) |
438 |
430 |
439 (* theory elements *) |
431 (* theory elements *) |
440 |
432 |
441 fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info); |
433 fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info); |
442 |
434 |
443 fun verbatim_source name mk_text = |
435 fun theory_source name mk_text = |
444 with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ()))); |
436 with_session () (fn _ => add_html_source name (HTML.theory_source (mk_text ()))); |
445 |
437 |
446 fun theory_output name s = |
438 fun theory_output name s = |
447 with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s)); |
439 with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s)); |
448 |
440 |
449 |
441 |
494 add_graph_entry (update_time, entry); |
486 add_graph_entry (update_time, entry); |
495 add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); |
487 add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); |
496 add_tex_index (update_time, Latex.theory_entry name); |
488 add_tex_index (update_time, Latex.theory_entry name); |
497 put_info {name = sess_name, session = path, is_local = is_some remote_path} thy |
489 put_info {name = sess_name, session = path, is_local = is_some remote_path} thy |
498 end); |
490 end); |
499 |
|
500 |
|
501 val hooks = ref ([]: (string -> (string * thm list) list -> unit) list); |
|
502 fun add_hook f = CRITICAL (fn () => change hooks (cons f)); |
|
503 |
|
504 fun results k xs = |
|
505 (List.app (fn f => (try (fn () => f k xs) (); ())) (! hooks); |
|
506 with_session () (fn _ => with_context add_html |
|
507 (HTML.results (ML_Context.the_local_context ()) k xs))); |
|
508 |
|
509 fun theorem a th = results Thm.theoremK [(a, [th])]; |
|
510 fun theorems a ths = results Thm.theoremK [(a, ths)]; |
|
511 fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s)); |
|
512 fun section s = with_session () (fn _ => with_context add_html (HTML.section s)); |
|
513 fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s)); |
|
514 fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s)); |
|
515 |
491 |
516 |
492 |
517 |
493 |
518 (** draft document output **) |
494 (** draft document output **) |
519 |
495 |