65 |
65 |
66 |
66 |
67 (* finish *) |
67 (* finish *) |
68 |
68 |
69 fun finish () = |
69 fun finish () = |
70 (Thy_Info.finish (); |
70 (Future.shutdown (); |
71 Present.finish (); |
71 Goal.finish_futures (); |
72 Keyword.status (); |
72 Thy_Info.finish (); |
73 Outer_Syntax.check_syntax (); |
73 Present.finish (); |
74 Future.shutdown (); |
74 Keyword.status (); |
75 Goal.finish_futures (); |
75 Outer_Syntax.check_syntax (); |
76 Goal.cancel_futures (); |
76 Goal.cancel_futures (); |
77 Future.shutdown (); |
77 Future.shutdown (); |
78 Options.reset_default (); |
78 Options.reset_default (); |
79 session_finished := true); |
79 session_finished := true); |
80 |
80 |
81 |
81 |
82 (* use_dir *) |
82 (* use_dir *) |
83 |
83 |
84 fun with_timing _ false f x = f x |
84 fun with_timing _ false f x = f x |
122 |
122 |
123 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent |
123 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent |
124 name dump rpath level timing verbose max_threads trace_threads |
124 name dump rpath level timing verbose max_threads trace_threads |
125 parallel_proofs parallel_proofs_threshold = |
125 parallel_proofs parallel_proofs_threshold = |
126 ((fn () => |
126 ((fn () => |
127 (Output.physical_stderr |
127 let |
128 "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n"; |
128 val _ = |
129 init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name |
129 Output.physical_stderr |
130 (doc_dump dump) rpath verbose; |
130 "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n"; |
131 with_timing item timing use root; |
131 val _ = |
132 finish ())) |
132 init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name |
|
133 (doc_dump dump) rpath verbose; |
|
134 val res1 = (use |> with_timing item timing |> Exn.capture) root; |
|
135 val res2 = Exn.capture finish (); |
|
136 in ignore (Par_Exn.release_all [res1, res2]) end) |
133 |> Unsynchronized.setmp Proofterm.proofs level |
137 |> Unsynchronized.setmp Proofterm.proofs level |
134 |> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) |
138 |> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) |
135 |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs |
139 |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs |
136 |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold |
140 |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold |
137 |> Unsynchronized.setmp Multithreading.trace trace_threads |
141 |> Unsynchronized.setmp Multithreading.trace trace_threads |