12 val get_theory: string -> theory |
12 val get_theory: string -> theory |
13 val master_directory: string -> Path.T |
13 val master_directory: string -> Path.T |
14 val remove_thy: string -> unit |
14 val remove_thy: string -> unit |
15 val use_thys: (string * Position.T) list -> unit |
15 val use_thys: (string * Position.T) list -> unit |
16 val use_thy: string * Position.T -> unit |
16 val use_thy: string * Position.T -> unit |
17 val use_thys_options: (Toplevel.transition -> Time.time option) -> Path.T -> |
17 val build_theories: (Toplevel.transition -> Time.time option) -> Path.T -> |
18 Options.T -> (string * Position.T) list -> unit |
18 Options.T * (string * Position.T) list -> unit |
19 val script_thy: Position.T -> string -> theory -> theory |
19 val script_thy: Position.T -> string -> theory -> theory |
20 val register_thy: theory -> unit |
20 val register_thy: theory -> unit |
21 val finish: unit -> unit |
21 val finish: unit -> unit |
22 end; |
22 end; |
23 |
23 |
340 schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty)); |
340 schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty)); |
341 |
341 |
342 val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current}; |
342 val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current}; |
343 val use_thy = use_thys o single; |
343 val use_thy = use_thys o single; |
344 |
344 |
345 fun use_thys_options last_timing master_dir options thys = |
345 |
346 (Options.set_default options; |
346 (* theories in batch build *) |
347 (use_theories { |
347 |
348 document = Present.document_enabled (Options.string options "document"), |
348 fun build_theories last_timing master_dir (options, thys) = |
349 last_timing = last_timing, |
349 let |
350 master_dir = master_dir} |
350 val condition = space_explode "," (Options.string options "condition"); |
351 |> Unsynchronized.setmp print_mode |
351 val conds = filter_out (can getenv_strict) condition; |
352 (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) |
352 in |
353 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") |
353 if null conds then |
354 |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") |
354 (Options.set_default options; |
355 |> Multithreading.max_threads_setmp (Options.int options "threads") |
355 (use_theories { |
356 |> Unsynchronized.setmp Future.ML_statistics true) thys); |
356 document = Present.document_enabled (Options.string options "document"), |
|
357 last_timing = last_timing, |
|
358 master_dir = master_dir} |
|
359 |> Unsynchronized.setmp print_mode |
|
360 (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) |
|
361 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") |
|
362 |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") |
|
363 |> Multithreading.max_threads_setmp (Options.int options "threads") |
|
364 |> Unsynchronized.setmp Future.ML_statistics true) thys) |
|
365 else |
|
366 Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
|
367 " (undefined " ^ commas conds ^ ")\n") |
|
368 end; |
357 |
369 |
358 |
370 |
359 (* toplevel scripting -- without maintaining database *) |
371 (* toplevel scripting -- without maintaining database *) |
360 |
372 |
361 fun script_thy pos txt thy = |
373 fun script_thy pos txt thy = |