author | wenzelm |
Sat, 30 Mar 2013 16:15:26 +0100 | |
changeset 51587 | 7050c4656fd8 |
parent 47653 | 4605d4341b8b |
child 55618 | 995162143ef4 |
permissions | -rw-r--r-- |
40393 | 1 |
/* Title: Pure/General/timing.scala |
46768 | 2 |
Module: PIDE |
40393 | 3 |
Author: Makarius |
4 |
||
5 |
Basic support for time measurement. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
45664 | 10 |
|
11 |
object Timing |
|
12 |
{ |
|
51587 | 13 |
val zero = Timing(Time.zero, Time.zero, Time.zero) |
14 |
||
47653 | 15 |
def timeit[A](message: String, enabled: Boolean = true)(e: => A) = |
16 |
if (enabled) { |
|
17 |
val start = java.lang.System.currentTimeMillis() |
|
18 |
val result = Exn.capture(e) |
|
19 |
val stop = java.lang.System.currentTimeMillis() |
|
46768 | 20 |
|
47653 | 21 |
val timing = Time.ms(stop - start) |
22 |
if (timing.is_relevant) |
|
23 |
java.lang.System.err.println( |
|
24 |
(if (message == null || message.isEmpty) "" else message + ": ") + |
|
25 |
timing.message + " elapsed time") |
|
46768 | 26 |
|
47653 | 27 |
Exn.release(result) |
28 |
} |
|
29 |
else e |
|
45664 | 30 |
} |
31 |
||
51587 | 32 |
sealed case class Timing(elapsed: Time, cpu: Time, gc: Time) |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
33 |
{ |
46768 | 34 |
def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant |
35 |
||
51587 | 36 |
def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc) |
37 |
||
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
38 |
def message: String = |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
39 |
elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" |
46768 | 40 |
|
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
41 |
override def toString = message |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
42 |
} |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
43 |