# 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