# HG changeset patch
# User wenzelm
# Date 1301517910 -7200
# Node ID e86b10c68f0b1872c02983a23cf1117523c5d7f2
# Parent  620343510c882b87980d9e712be4fe48f5a367e0
session timing: show pseudo-speedup factor;

diff -r 620343510c88 -r e86b10c68f0b src/Pure/System/session.ML
--- 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 ()))