# HG changeset patch
# User wenzelm
# Date 1384636665 -3600
# Node ID 96ccc8972fc7b225d80e991d8f400d8e4007fcc4
# Parent  bfba1352239a0a94bcea1ada4410c87cc31e08ec
prefer explicit "document" flag -- eliminated stateful Present.no_document;

diff -r bfba1352239a -r 96ccc8972fc7 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Nov 16 21:29:18 2013 +0100
+++ b/src/Pure/Thy/present.ML	Sat Nov 16 22:17:45 2013 +0100
@@ -7,7 +7,6 @@
 signature PRESENT =
 sig
   val session_name: theory -> string
-  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
   val read_variant: string -> string * string
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
@@ -138,9 +137,6 @@
 fun change_browser_info f =
   CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
 
-val suppress_tex_source = Unsynchronized.ref false;
-fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;
-
 fun init_theory_info name info =
   change_browser_info (fn (theories, tex_index, html_index, graph) =>
     (Symtab.update (name, info) theories, tex_index, html_index, graph));
@@ -165,10 +161,6 @@
   change_browser_info (fn (theories, tex_index, html_index, graph) =>
     (theories, tex_index, html_index, ins_graph_entry entry graph));
 
-fun put_tex_source name tex_source =
-  if ! suppress_tex_source then ()
-  else change_theory_info name (fn (_, html_source) => (tex_source, html_source));
-
 
 
 (** global session state **)
@@ -380,7 +372,8 @@
 (* theory elements *)
 
 fun theory_output name s =
-  with_session_info () (fn _ => put_tex_source name (Latex.isabelle_file name s));
+  with_session_info () (fn _ =>
+    change_theory_info name (fn (_, html_source) => (Latex.isabelle_file name s, html_source)));
 
 fun begin_theory update_time mk_text thy =
   with_session_info thy (fn {name = session_name, chapter, ...} =>
diff -r bfba1352239a -r 96ccc8972fc7 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Nov 16 21:29:18 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Nov 16 22:17:45 2013 +0100
@@ -17,7 +17,8 @@
   val loaded_files: string -> Path.T list
   val remove_thy: string -> unit
   val kill_thy: string -> unit
-  val use_theories: {last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
+  val use_theories:
+    {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
     (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
@@ -265,7 +266,7 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy last_timing initiators update_time deps text (name, pos) keywords parents =
+fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
   let
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -284,7 +285,7 @@
 
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
-      Thy_Load.load_thy last_timing update_time dir header text_pos text
+      Thy_Load.load_thy document last_timing update_time dir header text_pos text
         (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
   in
@@ -311,9 +312,9 @@
 
 in
 
-fun require_thys last_timing initiators dir strs tasks =
-      fold_map (require_thy last_timing initiators dir) strs tasks |>> forall I
-and require_thy last_timing initiators dir (str, require_pos) tasks =
+fun require_thys document last_timing initiators dir strs tasks =
+      fold_map (require_thy document last_timing initiators dir) strs tasks |>> forall I
+and require_thy document last_timing initiators dir (str, require_pos) tasks =
   let
     val path = Path.expand (Path.explode str);
     val name = Path.implode (Path.base path);
@@ -332,7 +333,7 @@
 
           val parents = map (base_name o #1) imports;
           val (parents_current, tasks') =
-            require_thys last_timing (name :: initiators)
+            require_thys document last_timing (name :: initiators)
               (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
@@ -345,7 +346,7 @@
                   let
                     val update_time = serial ();
                     val load =
-                      load_thy last_timing initiators update_time dep
+                      load_thy document last_timing initiators update_time dep
                         text (name, theory_pos) keywords;
                   in Task (parents, load) end);
 
@@ -358,10 +359,10 @@
 
 (* use_thy *)
 
-fun use_theories {last_timing, master_dir} imports =
-  schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
+fun use_theories {document, last_timing, master_dir} imports =
+  schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty));
 
-val use_thys = use_theories {last_timing = K NONE, master_dir = Path.current};
+val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
 val use_thy = use_thys o single;
 
 
@@ -371,7 +372,7 @@
   let
     val {name = (name, _), imports, ...} = header;
     val _ = kill_thy name;
-    val _ = use_theories {last_timing = K NONE, master_dir = master_dir} imports;
+    val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports;
     val _ = Thy_Header.define_keywords header;
     val parents = map (get_theory o base_name o fst) imports;
   in Thy_Load.begin_theory master_dir header parents end;
diff -r bfba1352239a -r 96ccc8972fc7 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 21:29:18 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 22:17:45 2013 +0100
@@ -20,8 +20,8 @@
   val loaded_files: theory -> Path.T list
   val loaded_files_current: theory -> bool
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
-  val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
-    Position.T -> string -> theory list -> theory * (unit -> unit) * int
+  val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
+    Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
 end;
 
 structure Thy_Load: THY_LOAD =
@@ -162,7 +162,7 @@
     val thy = Toplevel.end_theory end_pos end_state;
   in (results, thy) end;
 
-fun load_thy last_timing update_time master_dir header text_pos text parents =
+fun load_thy document last_timing update_time master_dir header text_pos text parents =
   let
     val time = ! Toplevel.timing;
 
@@ -191,10 +191,11 @@
         if exists (Toplevel.is_skipped_proof o #2) res then
           warning ("Cannot present theory with skipped proofs: " ^ quote name)
         else
-          Thy_Output.present_thy minor Keyword.command_tags
-            (Outer_Syntax.is_markup outer_syntax) res toks
-          |> Buffer.content
-          |> Present.theory_output name
+          let val tex_source =
+            Thy_Output.present_thy minor Keyword.command_tags
+              (Outer_Syntax.is_markup outer_syntax) res toks
+            |> Buffer.content;
+          in if document then Present.theory_output name tex_source else () end
       end;
 
   in (thy, present, size text) end;
diff -r bfba1352239a -r 96ccc8972fc7 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Nov 16 21:29:18 2013 +0100
+++ b/src/Pure/Tools/build.ML	Sat Nov 16 22:17:45 2013 +0100
@@ -97,18 +97,18 @@
 
 local
 
-fun no_document options =
-  (case Options.string options "document" of "" => true | "false" => true | _ => false);
-
 fun use_theories last_timing options =
-  Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
+  Thy_Info.use_theories {
+      document =
+        (case Options.string options "document" of "" => false | "false" => false | _ => true),
+      last_timing = last_timing,
+      master_dir = Path.current}
     |> Unsynchronized.setmp print_mode
         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     |> Unsynchronized.setmp Future.ML_statistics true
-    |> no_document options ? Present.no_document
     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");