--- a/src/Pure/Thy/thy_info.ML Sun Jan 11 21:06:47 2015 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Jan 13 21:46:09 2015 +0100
@@ -12,11 +12,10 @@
val get_theory: string -> theory
val master_directory: string -> Path.T
val remove_thy: string -> unit
- 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
+ val use_thys_options: (Toplevel.transition -> Time.time option) -> Path.T ->
+ Options.T -> (string * Position.T) list -> unit
val script_thy: Position.T -> string -> theory -> theory
val register_thy: theory -> unit
val finish: unit -> unit
@@ -343,6 +342,19 @@
val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
val use_thy = use_thys o single;
+fun use_thys_options last_timing master_dir options thys =
+ (Options.set_default options;
+ (use_theories {
+ document = Present.document_enabled (Options.string options "document"),
+ last_timing = last_timing,
+ master_dir = master_dir}
+ |> 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")
+ |> Multithreading.max_threads_setmp (Options.int options "threads")
+ |> Unsynchronized.setmp Future.ML_statistics true) thys);
+
(* toplevel scripting -- without maintaining database *)