src/Pure/Thy/present.ML
changeset 54456 f4b1440d9880
parent 54455 1d977436c1bf
child 54458 96ccc8972fc7
     1.1 --- a/src/Pure/Thy/present.ML	Sat Nov 16 20:20:09 2013 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sat Nov 16 21:18:31 2013 +0100
     1.3 @@ -12,10 +12,8 @@
     1.4    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     1.5      string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
     1.6    val finish: unit -> unit  (*not thread-safe!*)
     1.7 -  val init_theory: string -> unit
     1.8 -  val theory_source: string -> (unit -> HTML.text) -> unit
     1.9    val theory_output: string -> string -> unit
    1.10 -  val begin_theory: int -> theory -> theory
    1.11 +  val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    1.12    val display_drafts: Path.T list -> int
    1.13  end;
    1.14  
    1.15 @@ -105,15 +103,13 @@
    1.16  
    1.17  (* type theory_info *)
    1.18  
    1.19 -type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T};
    1.20 -
    1.21 -fun make_theory_info (tex_source, html_source, html) =
    1.22 -  {tex_source = tex_source, html_source = html_source, html = html}: theory_info;
    1.23 +type theory_info = {tex_source: string, html_source: string};
    1.24  
    1.25 -val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty);
    1.26 +fun make_theory_info (tex_source, html_source) =
    1.27 +  {tex_source = tex_source, html_source = html_source}: theory_info;
    1.28  
    1.29 -fun map_theory_info f {tex_source, html_source, html} =
    1.30 -  make_theory_info (f (tex_source, html_source, html));
    1.31 +fun map_theory_info f {tex_source, html_source} =
    1.32 +  make_theory_info (f (tex_source, html_source));
    1.33  
    1.34  
    1.35  (* type browser_info *)
    1.36 @@ -169,13 +165,9 @@
    1.37    change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.38      (theories, tex_index, html_index, ins_graph_entry entry graph));
    1.39  
    1.40 -fun add_tex_source name txt =
    1.41 +fun put_tex_source name tex_source =
    1.42    if ! suppress_tex_source then ()
    1.43 -  else change_theory_info name (fn (tex_source, html_source, html) =>
    1.44 -    (Buffer.add txt tex_source, html_source, html));
    1.45 -
    1.46 -fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
    1.47 -  (tex_source, Buffer.add txt html_source, html));
    1.48 +  else change_theory_info name (fn (_, html_source) => (tex_source, html_source));
    1.49  
    1.50  
    1.51  
    1.52 @@ -302,9 +294,8 @@
    1.53      val chapter_prefix = Path.append info_path (Path.basic chapter);
    1.54      val session_prefix = Path.append chapter_prefix (Path.basic name);
    1.55  
    1.56 -    fun finish_html (a, {html, ...}: theory_info) =
    1.57 -      File.write_buffer (Path.append session_prefix (html_path a))
    1.58 -        (Buffer.add HTML.end_document html);
    1.59 +    fun finish_html (a, {html_source, ...}: theory_info) =
    1.60 +      File.write (Path.append session_prefix (html_path a)) html_source;
    1.61  
    1.62      val sorted_graph = sorted_index graph;
    1.63      val opt_graphs =
    1.64 @@ -339,7 +330,8 @@
    1.65          (File.write (Path.append doc_dir graph_pdf_path) pdf;
    1.66            File.write (Path.append doc_dir graph_eps_path) eps));
    1.67        write_tex_index tex_index doc_dir;
    1.68 -      List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys);
    1.69 +      List.app (fn (a, {tex_source, ...}) =>
    1.70 +        write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys);
    1.71  
    1.72      val _ =
    1.73        if dump_prefix = "" then ()
    1.74 @@ -387,41 +379,35 @@
    1.75  
    1.76  (* theory elements *)
    1.77  
    1.78 -fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info);
    1.79 -
    1.80 -fun theory_source name mk_text =
    1.81 -  with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
    1.82 -
    1.83  fun theory_output name s =
    1.84 -  with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s));
    1.85 +  with_session_info () (fn _ => put_tex_source name (Latex.isabelle_file name s));
    1.86  
    1.87 -fun begin_theory update_time thy = with_session_info thy (fn {name = session_name, chapter, ...} =>
    1.88 -  let
    1.89 -    val name = Context.theory_name thy;
    1.90 -    val parents = Theory.parents_of thy;
    1.91 -    val parent_specs = parents |> map (fn parent =>
    1.92 -      (Option.map Url.File (theory_link (chapter, session_name) parent),
    1.93 -        (Context.theory_name parent)));
    1.94 +fun begin_theory update_time mk_text thy =
    1.95 +  with_session_info thy (fn {name = session_name, chapter, ...} =>
    1.96 +    let
    1.97 +      val name = Context.theory_name thy;
    1.98 +      val parents = Theory.parents_of thy;
    1.99 +
   1.100 +      val parent_specs = parents |> map (fn parent =>
   1.101 +        (Option.map Url.File (theory_link (chapter, session_name) parent),
   1.102 +          (Context.theory_name parent)));
   1.103 +      val html_source = HTML.theory name parent_specs (mk_text ());
   1.104  
   1.105 -    fun prep_html_source (tex_source, html_source, html) =
   1.106 -      let val txt = HTML.begin_theory name parent_specs (Buffer.content html_source)
   1.107 -      in (tex_source, Buffer.empty, Buffer.add txt html) end;
   1.108 -
   1.109 -    val entry =
   1.110 -     {name = name,
   1.111 -      ID = ID_of [chapter, session_name] name,
   1.112 -      dir = session_name,
   1.113 -      unfold = true,
   1.114 -      path = Path.implode (html_path name),
   1.115 -      parents = map ID_of_thy parents,
   1.116 -      content = []};
   1.117 -  in
   1.118 -    change_theory_info name prep_html_source;
   1.119 -    add_graph_entry (update_time, entry);
   1.120 -    add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
   1.121 -    add_tex_index (update_time, Latex.theory_entry name);
   1.122 -    Browser_Info.put {chapter = chapter, name = session_name} thy
   1.123 -  end);
   1.124 +      val graph_entry =
   1.125 +       {name = name,
   1.126 +        ID = ID_of [chapter, session_name] name,
   1.127 +        dir = session_name,
   1.128 +        unfold = true,
   1.129 +        path = Path.implode (html_path name),
   1.130 +        parents = map ID_of_thy parents,
   1.131 +        content = []};
   1.132 +    in
   1.133 +      init_theory_info name (make_theory_info ("", html_source));
   1.134 +      add_graph_entry (update_time, graph_entry);
   1.135 +      add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
   1.136 +      add_tex_index (update_time, Latex.theory_entry name);
   1.137 +      Browser_Info.put {chapter = chapter, name = session_name} thy
   1.138 +    end);
   1.139  
   1.140  
   1.141