export generated document.tex, unless explicit document=false;
authorwenzelm
Mon May 14 14:30:13 2018 +0200 (13 months ago)
changeset 6818134592bf86424
parent 68180 112d9624c020
child 68182 fa3cf61121ee
export generated document.tex, unless explicit document=false;
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/present.ML	Mon May 14 11:29:22 2018 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon May 14 14:30:13 2018 +0200
     1.3 @@ -8,12 +8,12 @@
     1.4  sig
     1.5    val get_bibtex_entries: theory -> string list
     1.6    val theory_qualifier: theory -> string
     1.7 -  val document_enabled: Options.T -> bool
     1.8 +  val document_option: Options.T -> {enabled: bool, disabled: bool}
     1.9    val document_variants: string -> (string * string) list
    1.10    val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
    1.11      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
    1.12    val finish: unit -> unit
    1.13 -  val theory_output: Position.T -> theory -> Latex.text list -> unit
    1.14 +  val theory_output: theory -> string list -> unit
    1.15    val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory
    1.16  end;
    1.17  
    1.18 @@ -56,7 +56,7 @@
    1.19  
    1.20  (* type theory_info *)
    1.21  
    1.22 -type theory_info = {tex_source: string, html_source: string};
    1.23 +type theory_info = {tex_source: string list, html_source: string};
    1.24  
    1.25  fun make_theory_info (tex_source, html_source) =
    1.26    {tex_source = tex_source, html_source = html_source}: theory_info;
    1.27 @@ -142,9 +142,11 @@
    1.28  
    1.29  (* options *)
    1.30  
    1.31 -fun document_enabled options =
    1.32 -  let val s = Options.string options "document"
    1.33 -  in s <> "" andalso s <> "false" end;
    1.34 +fun document_option options =
    1.35 +  (case Options.string options "document" of
    1.36 +    "" => {enabled = false, disabled = false}
    1.37 +  | "false" => {enabled = false, disabled = true}
    1.38 +  | _ => {enabled = true, disabled = false});
    1.39  
    1.40  fun document_variants str =
    1.41    let
    1.42 @@ -252,7 +254,7 @@
    1.43          val _ = write_tex_index tex_index doc_dir;
    1.44          val _ =
    1.45            List.app (fn (a, {tex_source, ...}) =>
    1.46 -            write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
    1.47 +            write_tex (fold Buffer.add tex_source Buffer.empty) a doc_dir) thys;
    1.48        in
    1.49          fn () =>
    1.50            (isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (),
    1.51 @@ -279,15 +281,10 @@
    1.52  
    1.53  (* theory elements *)
    1.54  
    1.55 -fun theory_output pos thy body =
    1.56 +fun theory_output thy output =
    1.57    with_session_info () (fn _ =>
    1.58      if is_session_theory thy then
    1.59 -      let val name = Context.theory_name thy in
    1.60 -        (change_theory_info name o apfst)
    1.61 -          (fn _ =>
    1.62 -            let val latex = Latex.isabelle_body name body
    1.63 -            in Latex.output_text latex ^ Latex.output_positions pos latex end)
    1.64 -      end
    1.65 +      (change_theory_info (Context.theory_name thy) o apfst) (K output)
    1.66      else ());
    1.67  
    1.68  fun theory_link (curr_chapter, curr_session) thy =
    1.69 @@ -312,7 +309,7 @@
    1.70            (Option.map Url.File (theory_link (chapter, session_name) parent),
    1.71              (Context.theory_name parent)));
    1.72        val html_source = HTML.theory symbols name parent_specs (mk_text ());
    1.73 -      val _ = init_theory_info name (make_theory_info ("", html_source));
    1.74 +      val _ = init_theory_info name (make_theory_info ([], html_source));
    1.75  
    1.76        val bibtex_entries' =
    1.77          if is_session_theory thy then
     2.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 14 11:29:22 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 14 14:30:13 2018 +0200
     2.3 @@ -53,8 +53,19 @@
     2.4    Theory.setup (add_presentation (fn {options, pos, segments} => fn thy =>
     2.5      if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
     2.6      else
     2.7 -      let val body = Thy_Output.present_thy thy segments;
     2.8 -      in if Present.document_enabled options then Present.theory_output pos thy body else () end));
     2.9 +      let
    2.10 +        val body = Thy_Output.present_thy thy segments;
    2.11 +        val option = Present.document_option options;
    2.12 +      in
    2.13 +        if #disabled option then ()
    2.14 +        else
    2.15 +          let
    2.16 +            val latex = Latex.isabelle_body (Context.theory_name thy) body;
    2.17 +            val output = [Latex.output_text latex, Latex.output_positions pos latex];
    2.18 +            val _ = Export.export thy "document.tex" output;
    2.19 +            val _ = if #enabled option then Present.theory_output thy output else ();
    2.20 +          in () end
    2.21 +      end));
    2.22  
    2.23  
    2.24