# HG changeset patch
# User wenzelm
# Date 1594477517 -7200
# Node ID 6c6609fd898c5f16c8d4cdc3e0cdb0ee49eb408c
# Parent  2550bac18b491e9c75beb64889d0af17f97c6dd0
more accurate message;

diff -r 2550bac18b49 -r 6c6609fd898c src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Sat Jul 11 15:52:54 2020 +0200
+++ b/src/Pure/General/timing.scala	Sat Jul 11 16:25:17 2020 +0200
@@ -35,6 +35,9 @@
     }
     else e
   }
+
+  def factor_format(f: Double): String =
+    String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
 }
 
 sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
@@ -56,11 +59,15 @@
   def message: String =
     elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
 
+  def message_factor: String =
+    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" +
+      Timing.factor_format(cpu.seconds / elapsed.seconds)
+
   def message_resources: String =
   {
     val factor_text =
       factor match {
-        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
+        case Some(f) => Timing.factor_format(f)
         case None => ""
       }
     if (resources.seconds >= 3.0)
diff -r 2550bac18b49 -r 6c6609fd898c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 11 15:52:54 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 11 16:25:17 2020 +0200
@@ -493,7 +493,7 @@
     "Finished " + session_name + " (" + timing.message_resources + ")"
 
   def session_timing(session_name: String, threads: Int, timing: Timing): String =
-    "Timing " + session_name + " (" + threads + " threads, " + timing.message_resources + ")"
+    "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
 
   def build(
     options: Options,