simplified HTML theory presentation;

--- a/src/Pure/Thy/html.ML	Sat Nov 16 20:20:09 2013 +0100
+++ b/src/Pure/Thy/html.ML	Sat Nov 16 21:18:31 2013 +0100
@@ -23,8 +23,7 @@
   val begin_session_index: string -> (Url.T * string) list -> Url.T -> text
   val applet_pages: string -> Url.T * string -> (string * string) list
   val theory_entry: Url.T * string -> text
-  val theory_source: text -> text
-  val begin_theory: string -> (Url.T option * string) list -> text -> text
+  val theory: string -> (Url.T option * string) list -> text -> text
 end;
 
 structure HTML: HTML =
@@ -320,13 +319,12 @@
 
 (* theory *)
 
-val theory_source = enclose
-  "\n</div>\n<div class=\"source\">\n<pre>"
-  "</pre>\n";
-
-fun begin_theory A Bs body =
-  begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A ^ "<br/>\n" ^
+fun theory A Bs txt =
+  begin_document ("Theory " ^ A) ^ "\n" ^
+  command "theory" ^ " " ^ name A ^ "<br/>\n" ^
   keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
-  "<br/>\n" ^ body;
+  "<br/>\n" ^
+  enclose "\n</div>\n<div class=\"source\">\n<pre>" "</pre>\n" txt ^
+  end_document;
 
 end;

--- 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);
 
 
 

--- 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);