equal
deleted
inserted
replaced
97 |
97 |
98 local |
98 local |
99 |
99 |
100 fun use_theories last_timing options = |
100 fun use_theories last_timing options = |
101 Thy_Info.use_theories { |
101 Thy_Info.use_theories { |
102 document = |
102 document = Present.document_enabled (Options.string options "document"), |
103 (case Options.string options "document" of "" => false | "false" => false | _ => true), |
|
104 last_timing = last_timing, |
103 last_timing = last_timing, |
105 master_dir = Path.current} |
104 master_dir = Path.current} |
106 |> Unsynchronized.setmp print_mode |
105 |> Unsynchronized.setmp print_mode |
107 (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) |
106 (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) |
108 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") |
107 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") |