equal
deleted
inserted
replaced
4 |
4 |
5 Basic support for time measurement. |
5 Basic support for time measurement. |
6 */ |
6 */ |
7 |
7 |
8 package isabelle |
8 package isabelle |
|
9 |
|
10 |
|
11 import java.util.Locale |
9 |
12 |
10 |
13 |
11 object Timing |
14 object Timing |
12 { |
15 { |
13 val zero = Timing(Time.zero, Time.zero, Time.zero) |
16 val zero = Timing(Time.zero, Time.zero, Time.zero) |
33 { |
36 { |
34 def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant |
37 def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant |
35 |
38 |
36 def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc) |
39 def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc) |
37 |
40 |
|
41 def message_resources: String = |
|
42 { |
|
43 val resources = cpu + gc |
|
44 val t1 = elapsed.seconds |
|
45 val t2 = resources.seconds |
|
46 val factor = |
|
47 if (t1 >= 5.0 && t2 >= 5.0) |
|
48 String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1)) |
|
49 else "" |
|
50 elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor |
|
51 } |
|
52 |
38 def message: String = |
53 def message: String = |
39 elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" |
54 elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" |
40 |
55 |
41 override def toString: String = message |
56 override def toString: String = message |
42 } |
57 } |
43 |
|