prefer explicit "document" flag -- eliminated stateful Present.no_document;
authorwenzelm
Sat Nov 16 22:17:45 2013 +0100 (2013-11-16)
changeset 5445896ccc8972fc7
parent 54457 bfba1352239a
child 54460 949a612097fb
prefer explicit "document" flag -- eliminated stateful Present.no_document;
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Thy/present.ML	Sat Nov 16 21:29:18 2013 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sat Nov 16 22:17:45 2013 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  signature PRESENT =
     1.5  sig
     1.6    val session_name: theory -> string
     1.7 -  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
     1.8    val read_variant: string -> string * string
     1.9    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    1.10      string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
    1.11 @@ -138,9 +137,6 @@
    1.12  fun change_browser_info f =
    1.13    CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
    1.14  
    1.15 -val suppress_tex_source = Unsynchronized.ref false;
    1.16 -fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;
    1.17 -
    1.18  fun init_theory_info name info =
    1.19    change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.20      (Symtab.update (name, info) theories, tex_index, html_index, graph));
    1.21 @@ -165,10 +161,6 @@
    1.22    change_browser_info (fn (theories, tex_index, html_index, graph) =>
    1.23      (theories, tex_index, html_index, ins_graph_entry entry graph));
    1.24  
    1.25 -fun put_tex_source name tex_source =
    1.26 -  if ! suppress_tex_source then ()
    1.27 -  else change_theory_info name (fn (_, html_source) => (tex_source, html_source));
    1.28 -
    1.29  
    1.30  
    1.31  (** global session state **)
    1.32 @@ -380,7 +372,8 @@
    1.33  (* theory elements *)
    1.34  
    1.35  fun theory_output name s =
    1.36 -  with_session_info () (fn _ => put_tex_source name (Latex.isabelle_file name s));
    1.37 +  with_session_info () (fn _ =>
    1.38 +    change_theory_info name (fn (_, html_source) => (Latex.isabelle_file name s, html_source)));
    1.39  
    1.40  fun begin_theory update_time mk_text thy =
    1.41    with_session_info thy (fn {name = session_name, chapter, ...} =>
     2.1 --- a/src/Pure/Thy/thy_info.ML	Sat Nov 16 21:29:18 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Nov 16 22:17:45 2013 +0100
     2.3 @@ -17,7 +17,8 @@
     2.4    val loaded_files: string -> Path.T list
     2.5    val remove_thy: string -> unit
     2.6    val kill_thy: string -> unit
     2.7 -  val use_theories: {last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
     2.8 +  val use_theories:
     2.9 +    {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
    2.10      (string * Position.T) list -> unit
    2.11    val use_thys: (string * Position.T) list -> unit
    2.12    val use_thy: string * Position.T -> unit
    2.13 @@ -265,7 +266,7 @@
    2.14  fun required_by _ [] = ""
    2.15    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
    2.16  
    2.17 -fun load_thy last_timing initiators update_time deps text (name, pos) keywords parents =
    2.18 +fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
    2.19    let
    2.20      val _ = kill_thy name;
    2.21      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
    2.22 @@ -284,7 +285,7 @@
    2.23  
    2.24      val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
    2.25      val (theory, present, weight) =
    2.26 -      Thy_Load.load_thy last_timing update_time dir header text_pos text
    2.27 +      Thy_Load.load_thy document last_timing update_time dir header text_pos text
    2.28          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
    2.29      fun commit () = update_thy deps theory;
    2.30    in
    2.31 @@ -311,9 +312,9 @@
    2.32  
    2.33  in
    2.34  
    2.35 -fun require_thys last_timing initiators dir strs tasks =
    2.36 -      fold_map (require_thy last_timing initiators dir) strs tasks |>> forall I
    2.37 -and require_thy last_timing initiators dir (str, require_pos) tasks =
    2.38 +fun require_thys document last_timing initiators dir strs tasks =
    2.39 +      fold_map (require_thy document last_timing initiators dir) strs tasks |>> forall I
    2.40 +and require_thy document last_timing initiators dir (str, require_pos) tasks =
    2.41    let
    2.42      val path = Path.expand (Path.explode str);
    2.43      val name = Path.implode (Path.base path);
    2.44 @@ -332,7 +333,7 @@
    2.45  
    2.46            val parents = map (base_name o #1) imports;
    2.47            val (parents_current, tasks') =
    2.48 -            require_thys last_timing (name :: initiators)
    2.49 +            require_thys document last_timing (name :: initiators)
    2.50                (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
    2.51  
    2.52            val all_current = current andalso parents_current;
    2.53 @@ -345,7 +346,7 @@
    2.54                    let
    2.55                      val update_time = serial ();
    2.56                      val load =
    2.57 -                      load_thy last_timing initiators update_time dep
    2.58 +                      load_thy document last_timing initiators update_time dep
    2.59                          text (name, theory_pos) keywords;
    2.60                    in Task (parents, load) end);
    2.61  
    2.62 @@ -358,10 +359,10 @@
    2.63  
    2.64  (* use_thy *)
    2.65  
    2.66 -fun use_theories {last_timing, master_dir} imports =
    2.67 -  schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
    2.68 +fun use_theories {document, last_timing, master_dir} imports =
    2.69 +  schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty));
    2.70  
    2.71 -val use_thys = use_theories {last_timing = K NONE, master_dir = Path.current};
    2.72 +val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
    2.73  val use_thy = use_thys o single;
    2.74  
    2.75  
    2.76 @@ -371,7 +372,7 @@
    2.77    let
    2.78      val {name = (name, _), imports, ...} = header;
    2.79      val _ = kill_thy name;
    2.80 -    val _ = use_theories {last_timing = K NONE, master_dir = master_dir} imports;
    2.81 +    val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports;
    2.82      val _ = Thy_Header.define_keywords header;
    2.83      val parents = map (get_theory o base_name o fst) imports;
    2.84    in Thy_Load.begin_theory master_dir header parents end;
     3.1 --- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 21:29:18 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 22:17:45 2013 +0100
     3.3 @@ -20,8 +20,8 @@
     3.4    val loaded_files: theory -> Path.T list
     3.5    val loaded_files_current: theory -> bool
     3.6    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     3.7 -  val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
     3.8 -    Position.T -> string -> theory list -> theory * (unit -> unit) * int
     3.9 +  val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
    3.10 +    Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
    3.11  end;
    3.12  
    3.13  structure Thy_Load: THY_LOAD =
    3.14 @@ -162,7 +162,7 @@
    3.15      val thy = Toplevel.end_theory end_pos end_state;
    3.16    in (results, thy) end;
    3.17  
    3.18 -fun load_thy last_timing update_time master_dir header text_pos text parents =
    3.19 +fun load_thy document last_timing update_time master_dir header text_pos text parents =
    3.20    let
    3.21      val time = ! Toplevel.timing;
    3.22  
    3.23 @@ -191,10 +191,11 @@
    3.24          if exists (Toplevel.is_skipped_proof o #2) res then
    3.25            warning ("Cannot present theory with skipped proofs: " ^ quote name)
    3.26          else
    3.27 -          Thy_Output.present_thy minor Keyword.command_tags
    3.28 -            (Outer_Syntax.is_markup outer_syntax) res toks
    3.29 -          |> Buffer.content
    3.30 -          |> Present.theory_output name
    3.31 +          let val tex_source =
    3.32 +            Thy_Output.present_thy minor Keyword.command_tags
    3.33 +              (Outer_Syntax.is_markup outer_syntax) res toks
    3.34 +            |> Buffer.content;
    3.35 +          in if document then Present.theory_output name tex_source else () end
    3.36        end;
    3.37  
    3.38    in (thy, present, size text) end;
     4.1 --- a/src/Pure/Tools/build.ML	Sat Nov 16 21:29:18 2013 +0100
     4.2 +++ b/src/Pure/Tools/build.ML	Sat Nov 16 22:17:45 2013 +0100
     4.3 @@ -97,18 +97,18 @@
     4.4  
     4.5  local
     4.6  
     4.7 -fun no_document options =
     4.8 -  (case Options.string options "document" of "" => true | "false" => true | _ => false);
     4.9 -
    4.10  fun use_theories last_timing options =
    4.11 -  Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
    4.12 +  Thy_Info.use_theories {
    4.13 +      document =
    4.14 +        (case Options.string options "document" of "" => false | "false" => false | _ => true),
    4.15 +      last_timing = last_timing,
    4.16 +      master_dir = Path.current}
    4.17      |> Unsynchronized.setmp print_mode
    4.18          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    4.19      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    4.20      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    4.21      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    4.22      |> Unsynchronized.setmp Future.ML_statistics true
    4.23 -    |> no_document options ? Present.no_document
    4.24      |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    4.25      |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    4.26