equal
deleted
inserted
replaced
44 |> the_default Time.zeroTime; |
44 |> the_default Time.zeroTime; |
45 |
45 |
46 |
46 |
47 (* session timing *) |
47 (* session timing *) |
48 |
48 |
49 fun session_timing session_name verbose f x = |
49 fun session_timing f x = |
50 let |
50 let |
51 val start = Timing.start (); |
51 val start = Timing.start (); |
52 val y = f x; |
52 val y = f x; |
53 val timing = Timing.result start; |
53 val timing = Timing.result start; |
54 |
54 |
55 val threads = string_of_int (Multithreading.max_threads ()); |
55 val threads = string_of_int (Multithreading.max_threads ()); |
56 val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |
56 val props = [("threads", threads)] @ Markup.timing_properties timing; |
57 |> Real.fmt (StringCvt.FIX (SOME 2)); |
57 val _ = Output.protocol_message (Markup.session_timing :: props) []; |
58 |
|
59 val timing_props = [("threads", threads)] @ Markup.timing_properties timing; |
|
60 val _ = Output.protocol_message (Markup.session_timing :: timing_props) []; |
|
61 val _ = |
|
62 if verbose then |
|
63 Output.physical_stderr ("Timing " ^ session_name ^ " (" ^ |
|
64 threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") |
|
65 else (); |
|
66 in y end; |
58 in y end; |
67 |
59 |
68 |
60 |
69 (* protocol messages *) |
61 (* protocol messages *) |
70 |
62 |
209 val last_timing = get_timings (fold update_timings command_timings empty_timings); |
201 val last_timing = get_timings (fold update_timings command_timings empty_timings); |
210 |
202 |
211 val res1 = |
203 val res1 = |
212 theories |> |
204 theories |> |
213 (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir) |
205 (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir) |
214 |> session_timing session_name verbose |
206 |> session_timing |
215 |> Exn.capture); |
207 |> Exn.capture); |
216 val res2 = Exn.capture Session.finish (); |
208 val res2 = Exn.capture Session.finish (); |
217 |
209 |
218 val _ = Resources.finish_session_base (); |
210 val _ = Resources.finish_session_base (); |
219 val _ = Par_Exn.release_all [res1, res2]; |
211 val _ = Par_Exn.release_all [res1, res2]; |