23 string -> (bool * Path.T) option -> Url.T option * bool -> bool -> unit |
23 string -> (bool * Path.T) option -> Url.T option * bool -> bool -> 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 option -> string -> string list -> |
28 val begin_theory: Path.T list -> string -> string list -> |
29 (Path.T * bool) list -> theory -> theory |
29 (Path.T * bool) list -> theory -> theory |
30 val add_hook: (string -> (string * thm list) list -> unit) -> unit |
30 val add_hook: (string -> (string * thm list) list -> unit) -> unit |
31 val results: string -> (string * thm list) list -> unit |
31 val results: string -> (string * thm list) list -> unit |
32 val theorem: string -> thm -> unit |
32 val theorem: string -> thm -> unit |
33 val theorems: string -> thm list -> unit |
33 val theorems: string -> thm list -> unit |
125 Url.implode (Url.append (the remote_path) (Url.File |
125 Url.implode (Url.append (the remote_path) (Url.File |
126 (Path.append (Path.make session) (html_path name)))) |
126 (Path.append (Path.make session) (html_path name)))) |
127 else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)), |
127 else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)), |
128 unfold = false, |
128 unfold = false, |
129 parents = |
129 parents = |
130 map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)} |
130 map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_parents name)} |
131 end) (ThyInfo.names ()); |
131 end) (ThyInfo.names ()); |
132 |
132 |
133 fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) = |
133 fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) = |
134 filter_out (fn entry' => #ID entry' = ID) gr @ [entry]; |
134 filter_out (fn entry' => #ID entry' = ID) gr @ [entry]; |
135 |
135 |
450 (Path.append (Path.make session) (html_path name))) |
450 (Path.append (Path.make session) (html_path name))) |
451 else Url.File (Path.append (mk_rel_path curr_session session) |
451 else Url.File (Path.append (mk_rel_path curr_session session) |
452 (html_path name))), name) |
452 (html_path name))), name) |
453 end; |
453 end; |
454 |
454 |
455 fun begin_theory optpath name raw_parents orig_files thy = |
455 fun begin_theory dirs name raw_parents orig_files thy = |
456 with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => |
456 with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => |
457 let |
457 let |
458 val parents = map (parent_link remote_path path) raw_parents; |
458 val parents = map (parent_link remote_path path) raw_parents; |
459 val ml_path = ThyLoad.ml_path name; |
459 val ml_path = ThyLoad.ml_path name; |
460 val files = map (apsnd SOME) orig_files @ |
460 val files = map (apsnd SOME) orig_files @ |
461 (if is_some (ThyLoad.check_file optpath ml_path) then [(ml_path, NONE)] else []); |
461 (if is_some (ThyLoad.check_file dirs ml_path) then [(ml_path, NONE)] else []); |
462 |
462 |
463 fun prep_file (raw_path, loadit) = |
463 fun prep_file (raw_path, loadit) = |
464 (case ThyLoad.check_file optpath raw_path of |
464 (case ThyLoad.check_ml dirs raw_path of |
465 SOME (path, _) => |
465 SOME (path, _) => |
466 let |
466 let |
467 val base = Path.base path; |
467 val base = Path.base path; |
468 val base_html = html_ext base; |
468 val base_html = html_ext base; |
469 in |
469 in |