clarified signature: more explicit type "context" with full options;
authorwenzelm
Mon May 14 10:58:14 2018 +0200 (12 months ago)
changeset 68179da70c9e91135
parent 68178 e3dd94d04eee
child 68180 112d9624c020
clarified signature: more explicit type "context" with full options;
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Thy/present.ML	Mon May 14 10:22:45 2018 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon May 14 10:58:14 2018 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    val get_bibtex_entries: theory -> string list
     1.6    val theory_qualifier: theory -> string
     1.7 -  val document_enabled: string -> bool
     1.8 +  val document_enabled: Options.T -> 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 @@ -142,7 +142,9 @@
    1.13  
    1.14  (* options *)
    1.15  
    1.16 -fun document_enabled s = s <> "" andalso s <> "false";
    1.17 +fun document_enabled options =
    1.18 +  let val s = Options.string options "document"
    1.19 +  in s <> "" andalso s <> "false" end;
    1.20  
    1.21  fun document_variants str =
    1.22    let
     2.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 14 10:22:45 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 14 10:58:14 2018 +0200
     2.3 @@ -14,13 +14,12 @@
     2.4    val get_theory: string -> theory
     2.5    val master_directory: string -> Path.T
     2.6    val remove_thy: string -> unit
     2.7 -  val use_theories:
     2.8 -    {document: bool,
     2.9 +  type context =
    2.10 +    {options: Options.T,
    2.11       symbols: HTML.symbols,
    2.12       bibtex_entries: string list,
    2.13 -     last_timing: Toplevel.transition -> Time.time,
    2.14 -     qualifier: string,
    2.15 -     master_dir: Path.T} -> (string * Position.T) list -> unit
    2.16 +     last_timing: Toplevel.transition -> Time.time}
    2.17 +  val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
    2.18    val use_thy: string -> unit
    2.19    val script_thy: Position.T -> string -> theory -> theory
    2.20    val register_thy: theory -> unit
    2.21 @@ -155,6 +154,21 @@
    2.22  fun update_thy deps theory = change_thys (update deps theory);
    2.23  
    2.24  
    2.25 +(* context *)
    2.26 +
    2.27 +type context =
    2.28 +  {options: Options.T,
    2.29 +   symbols: HTML.symbols,
    2.30 +   bibtex_entries: string list,
    2.31 +   last_timing: Toplevel.transition -> Time.time};
    2.32 +
    2.33 +fun default_context (): context =
    2.34 +  {options = Options.default (),
    2.35 +   symbols = HTML.no_symbols,
    2.36 +   bibtex_entries = [],
    2.37 +   last_timing = K Time.zeroTime};
    2.38 +
    2.39 +
    2.40  (* scheduling loader tasks *)
    2.41  
    2.42  datatype result =
    2.43 @@ -259,9 +273,9 @@
    2.44      val thy = Toplevel.end_theory end_pos end_state;
    2.45    in (results, thy) end;
    2.46  
    2.47 -fun eval_thy {document, symbols, bibtex_entries, last_timing} update_time master_dir header
    2.48 -    text_pos text parents =
    2.49 +fun eval_thy (context: context) update_time master_dir header text_pos text parents =
    2.50    let
    2.51 +    val {options, symbols, bibtex_entries, last_timing} = context;
    2.52      val (name, _) = #name header;
    2.53      val keywords =
    2.54        fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
    2.55 @@ -288,7 +302,7 @@
    2.56          if exists (Toplevel.is_skipped_proof o #result_state) segments then ()
    2.57          else
    2.58            let val body = Thy_Output.present_thy thy segments;
    2.59 -          in if document then Present.theory_output text_pos thy body else () end
    2.60 +          in if Present.document_enabled options then Present.theory_output text_pos thy body else () end
    2.61        end;
    2.62    in (thy, present, size text) end;
    2.63  
    2.64 @@ -401,20 +415,13 @@
    2.65  
    2.66  (* use theories *)
    2.67  
    2.68 -fun use_theories {document, symbols, bibtex_entries, last_timing, qualifier, master_dir} imports =
    2.69 -  let
    2.70 -    val context =
    2.71 -      {document = document, symbols = symbols, bibtex_entries = bibtex_entries,
    2.72 -        last_timing = last_timing};
    2.73 -    val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty;
    2.74 +fun use_theories context qualifier master_dir imports =
    2.75 +  let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty
    2.76    in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
    2.77  
    2.78  fun use_thy name =
    2.79 -  use_theories
    2.80 -    {document = false, symbols = HTML.no_symbols, bibtex_entries = [],
    2.81 -      last_timing = K Time.zeroTime, qualifier = Resources.default_qualifier,
    2.82 -      master_dir = Path.current}
    2.83 -    [(name, Position.none)];
    2.84 +  use_theories (default_context ()) Resources.default_qualifier
    2.85 +    Path.current [(name, Position.none)];
    2.86  
    2.87  
    2.88  (* toplevel scripting -- without maintaining database *)
     3.1 --- a/src/Pure/Tools/build.ML	Mon May 14 10:22:45 2018 +0200
     3.2 +++ b/src/Pure/Tools/build.ML	Mon May 14 10:58:14 2018 +0200
     3.3 @@ -113,6 +113,9 @@
     3.4  
     3.5  fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
     3.6    let
     3.7 +    val context =
     3.8 +      {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
     3.9 +        last_timing = last_timing};
    3.10      val condition = space_explode "," (Options.string options "condition");
    3.11      val conds = filter_out (can getenv_strict) condition;
    3.12    in
    3.13 @@ -121,13 +124,7 @@
    3.14          Options.set_default options;
    3.15          Isabelle_Process.init_options ();
    3.16          Future.fork I;
    3.17 -        (Thy_Info.use_theories {
    3.18 -          document = Present.document_enabled (Options.string options "document"),
    3.19 -          symbols = symbols,
    3.20 -          bibtex_entries = bibtex_entries,
    3.21 -          last_timing = last_timing,
    3.22 -          qualifier = qualifier,
    3.23 -          master_dir = master_dir}
    3.24 +        (Thy_Info.use_theories context qualifier master_dir
    3.25          |>
    3.26            (case Options.string options "profiling" of
    3.27              "" => I