--- a/src/Pure/System/session.ML Wed Mar 30 22:06:25 2011 +0200
+++ b/src/Pure/System/session.ML Wed Mar 30 22:45:10 2011 +0200
@@ -103,10 +103,13 @@
let
val start = Timing.start ();
val _ = use root;
+ val timing = Timing.result start;
+ val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
+ |> Real.fmt (StringCvt.FIX (SOME 2));
val _ =
Output.raw_stderr ("Timing " ^ item ^ " (" ^
string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
- Timing.message (Timing.result start) ^ ")\n");
+ Timing.message timing ^ ", factor " ^ factor ^ ")\n");
in () end
else use root;
finish ()))