--- a/src/Pure/General/time.scala Wed Mar 09 16:40:39 2016 +0100
+++ b/src/Pure/General/time.scala Wed Mar 09 16:42:30 2016 +0100
@@ -46,5 +46,11 @@
override def toString: String = Time.print_seconds(seconds)
def message: String = toString + "s"
+
+ def message_hms: String =
+ {
+ val s = ms / 1000
+ String.format(Locale.ROOT, "%d:%02d:%02d",
+ new java.lang.Long(s / 3600), new java.lang.Long((s / 60) % 60), new java.lang.Long(s % 60))
+ }
}
-
--- a/src/Pure/General/timing.scala Wed Mar 09 16:40:39 2016 +0100
+++ b/src/Pure/General/timing.scala Wed Mar 09 16:42:30 2016 +0100
@@ -8,6 +8,9 @@
package isabelle
+import java.util.Locale
+
+
object Timing
{
val zero = Timing(Time.zero, Time.zero, Time.zero)
@@ -35,9 +38,20 @@
def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
+ def message_resources: String =
+ {
+ val resources = cpu + gc
+ val t1 = elapsed.seconds
+ val t2 = resources.seconds
+ val factor =
+ if (t1 >= 5.0 && t2 >= 5.0)
+ String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
+ else ""
+ elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
+ }
+
def message: String =
elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
override def toString: String = message
}
-