# HG changeset patch # User wenzelm # Date 1457538150 -3600 # Node ID 2fd90993a92810586325a576e7621954e89b2c91 # Parent f4c96158a3b8f21dae14a743282ab3c2f306d3b6 print timing like lib/scripts/timestop.bash; diff -r f4c96158a3b8 -r 2fd90993a928 src/Pure/General/time.scala --- 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)) + } } - diff -r f4c96158a3b8 -r 2fd90993a928 src/Pure/General/timing.scala --- 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 } -