\n
" "
\n" txt ^
+ end_document;
end;
diff -r 1d977436c1bf -r f4b1440d9880 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML Sat Nov 16 20:20:09 2013 +0100
+++ b/src/Pure/Thy/present.ML Sat Nov 16 21:18:31 2013 +0100
@@ -12,10 +12,8 @@
val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
string * string -> bool * string -> bool -> theory list -> unit (*not thread-safe!*)
val finish: unit -> unit (*not thread-safe!*)
- val init_theory: string -> unit
- val theory_source: string -> (unit -> HTML.text) -> unit
val theory_output: string -> string -> unit
- val begin_theory: int -> theory -> theory
+ val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
val display_drafts: Path.T list -> int
end;
@@ -105,15 +103,13 @@
(* type theory_info *)
-type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T};
-
-fun make_theory_info (tex_source, html_source, html) =
- {tex_source = tex_source, html_source = html_source, html = html}: theory_info;
+type theory_info = {tex_source: string, html_source: string};
-val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty);
+fun make_theory_info (tex_source, html_source) =
+ {tex_source = tex_source, html_source = html_source}: theory_info;
-fun map_theory_info f {tex_source, html_source, html} =
- make_theory_info (f (tex_source, html_source, html));
+fun map_theory_info f {tex_source, html_source} =
+ make_theory_info (f (tex_source, html_source));
(* type browser_info *)
@@ -169,13 +165,9 @@
change_browser_info (fn (theories, tex_index, html_index, graph) =>
(theories, tex_index, html_index, ins_graph_entry entry graph));
-fun add_tex_source name txt =
+fun put_tex_source name tex_source =
if ! suppress_tex_source then ()
- else change_theory_info name (fn (tex_source, html_source, html) =>
- (Buffer.add txt tex_source, html_source, html));
-
-fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
- (tex_source, Buffer.add txt html_source, html));
+ else change_theory_info name (fn (_, html_source) => (tex_source, html_source));
@@ -302,9 +294,8 @@
val chapter_prefix = Path.append info_path (Path.basic chapter);
val session_prefix = Path.append chapter_prefix (Path.basic name);
- fun finish_html (a, {html, ...}: theory_info) =
- File.write_buffer (Path.append session_prefix (html_path a))
- (Buffer.add HTML.end_document html);
+ fun finish_html (a, {html_source, ...}: theory_info) =
+ File.write (Path.append session_prefix (html_path a)) html_source;
val sorted_graph = sorted_index graph;
val opt_graphs =
@@ -339,7 +330,8 @@
(File.write (Path.append doc_dir graph_pdf_path) pdf;
File.write (Path.append doc_dir graph_eps_path) eps));
write_tex_index tex_index doc_dir;
- List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys);
+ List.app (fn (a, {tex_source, ...}) =>
+ write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys);
val _ =
if dump_prefix = "" then ()
@@ -387,41 +379,35 @@
(* theory elements *)
-fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info);
-
-fun theory_source name mk_text =
- with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
-
fun theory_output name s =
- with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s));
+ with_session_info () (fn _ => put_tex_source name (Latex.isabelle_file name s));
-fun begin_theory update_time thy = with_session_info thy (fn {name = session_name, chapter, ...} =>
- let
- val name = Context.theory_name thy;
- val parents = Theory.parents_of thy;
- val parent_specs = parents |> map (fn parent =>
- (Option.map Url.File (theory_link (chapter, session_name) parent),
- (Context.theory_name parent)));
+fun begin_theory update_time mk_text thy =
+ with_session_info thy (fn {name = session_name, chapter, ...} =>
+ let
+ val name = Context.theory_name thy;
+ val parents = Theory.parents_of thy;
+
+ val parent_specs = parents |> map (fn parent =>
+ (Option.map Url.File (theory_link (chapter, session_name) parent),
+ (Context.theory_name parent)));
+ val html_source = HTML.theory name parent_specs (mk_text ());
- fun prep_html_source (tex_source, html_source, html) =
- let val txt = HTML.begin_theory name parent_specs (Buffer.content html_source)
- in (tex_source, Buffer.empty, Buffer.add txt html) end;
-
- val entry =
- {name = name,
- ID = ID_of [chapter, session_name] name,
- dir = session_name,
- unfold = true,
- path = Path.implode (html_path name),
- parents = map ID_of_thy parents,
- content = []};
- in
- change_theory_info name prep_html_source;
- add_graph_entry (update_time, entry);
- add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
- add_tex_index (update_time, Latex.theory_entry name);
- Browser_Info.put {chapter = chapter, name = session_name} thy
- end);
+ val graph_entry =
+ {name = name,
+ ID = ID_of [chapter, session_name] name,
+ dir = session_name,
+ unfold = true,
+ path = Path.implode (html_path name),
+ parents = map ID_of_thy parents,
+ content = []};
+ in
+ init_theory_info name (make_theory_info ("", html_source));
+ add_graph_entry (update_time, graph_entry);
+ add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
+ add_tex_index (update_time, Latex.theory_entry name);
+ Browser_Info.put {chapter = chapter, name = session_name} thy
+ end);
diff -r 1d977436c1bf -r f4b1440d9880 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML Sat Nov 16 20:20:09 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Sat Nov 16 21:18:31 2013 +0100
@@ -168,19 +168,16 @@
val {name = (name, _), ...} = header;
val _ = Thy_Header.define_keywords header;
- val _ = Present.init_theory name;
- fun init () =
- begin_theory master_dir header parents
- |> Present.begin_theory update_time;
val lexs = Keyword.get_lexicons ();
-
val toks = Thy_Syntax.parse_tokens lexs text_pos text;
val spans = map (Thy_Syntax.resolve_files (read_files master_dir)) (Thy_Syntax.parse_spans toks);
val elements = Thy_Syntax.parse_elements spans;
- val _ = Present.theory_source name
- (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
+ fun init () =
+ begin_theory master_dir header parents
+ |> Present.begin_theory update_time
+ (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);