# HG changeset patch
# User wenzelm
# Date 1526288294 -7200
# Node ID da70c9e91135e2c5ae5c7961b82883a10a6bdecb
# Parent  e3dd94d04eeea832ddd953f72dc4bbf7c0252676
clarified signature: more explicit type "context" with full options;

diff -r e3dd94d04eee -r da70c9e91135 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon May 14 10:22:45 2018 +0200
+++ b/src/Pure/Thy/present.ML	Mon May 14 10:58:14 2018 +0200
@@ -8,7 +8,7 @@
 sig
   val get_bibtex_entries: theory -> string list
   val theory_qualifier: theory -> string
-  val document_enabled: string -> bool
+  val document_enabled: Options.T -> bool
   val document_variants: string -> (string * string) list
   val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
@@ -142,7 +142,9 @@
 
 (* options *)
 
-fun document_enabled s = s <> "" andalso s <> "false";
+fun document_enabled options =
+  let val s = Options.string options "document"
+  in s <> "" andalso s <> "false" end;
 
 fun document_variants str =
   let
diff -r e3dd94d04eee -r da70c9e91135 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon May 14 10:22:45 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon May 14 10:58:14 2018 +0200
@@ -14,13 +14,12 @@
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
-  val use_theories:
-    {document: bool,
+  type context =
+    {options: Options.T,
      symbols: HTML.symbols,
      bibtex_entries: string list,
-     last_timing: Toplevel.transition -> Time.time,
-     qualifier: string,
-     master_dir: Path.T} -> (string * Position.T) list -> unit
+     last_timing: Toplevel.transition -> Time.time}
+  val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
@@ -155,6 +154,21 @@
 fun update_thy deps theory = change_thys (update deps theory);
 
 
+(* context *)
+
+type context =
+  {options: Options.T,
+   symbols: HTML.symbols,
+   bibtex_entries: string list,
+   last_timing: Toplevel.transition -> Time.time};
+
+fun default_context (): context =
+  {options = Options.default (),
+   symbols = HTML.no_symbols,
+   bibtex_entries = [],
+   last_timing = K Time.zeroTime};
+
+
 (* scheduling loader tasks *)
 
 datatype result =
@@ -259,9 +273,9 @@
     val thy = Toplevel.end_theory end_pos end_state;
   in (results, thy) end;
 
-fun eval_thy {document, symbols, bibtex_entries, last_timing} update_time master_dir header
-    text_pos text parents =
+fun eval_thy (context: context) update_time master_dir header text_pos text parents =
   let
+    val {options, symbols, bibtex_entries, last_timing} = context;
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
@@ -288,7 +302,7 @@
         if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
         else
           let val body = Thy_Output.present_thy thy segments;
-          in if document then Present.theory_output text_pos thy body else () end
+          in if Present.document_enabled options then Present.theory_output text_pos thy body else () end
       end;
   in (thy, present, size text) end;
 
@@ -401,20 +415,13 @@
 
 (* use theories *)
 
-fun use_theories {document, symbols, bibtex_entries, last_timing, qualifier, master_dir} imports =
-  let
-    val context =
-      {document = document, symbols = symbols, bibtex_entries = bibtex_entries,
-        last_timing = last_timing};
-    val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty;
+fun use_theories context qualifier master_dir imports =
+  let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty
   in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
-  use_theories
-    {document = false, symbols = HTML.no_symbols, bibtex_entries = [],
-      last_timing = K Time.zeroTime, qualifier = Resources.default_qualifier,
-      master_dir = Path.current}
-    [(name, Position.none)];
+  use_theories (default_context ()) Resources.default_qualifier
+    Path.current [(name, Position.none)];
 
 
 (* toplevel scripting -- without maintaining database *)
diff -r e3dd94d04eee -r da70c9e91135 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon May 14 10:22:45 2018 +0200
+++ b/src/Pure/Tools/build.ML	Mon May 14 10:58:14 2018 +0200
@@ -113,6 +113,9 @@
 
 fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
   let
+    val context =
+      {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
+        last_timing = last_timing};
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
   in
@@ -121,13 +124,7 @@
         Options.set_default options;
         Isabelle_Process.init_options ();
         Future.fork I;
-        (Thy_Info.use_theories {
-          document = Present.document_enabled (Options.string options "document"),
-          symbols = symbols,
-          bibtex_entries = bibtex_entries,
-          last_timing = last_timing,
-          qualifier = qualifier,
-          master_dir = master_dir}
+        (Thy_Info.use_theories context qualifier master_dir
         |>
           (case Options.string options "profiling" of
             "" => I