--- 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)
--- 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,