diff -r 69b31dc7256e -r ad5d7461b370 src/Pure/General/timing.scala --- a/src/Pure/General/timing.scala Thu Apr 24 10:38:14 2014 +0200 +++ b/src/Pure/General/timing.scala Thu Apr 24 11:01:14 2014 +0200 @@ -14,11 +14,11 @@ def timeit[A](message: String, enabled: Boolean = true)(e: => A) = if (enabled) { - val start = System.currentTimeMillis() + val start = Time.now() val result = Exn.capture(e) - val stop = System.currentTimeMillis() + val stop = Time.now() - val timing = Time.ms(stop - start) + val timing = stop - start if (timing.is_relevant) System.err.println( (if (message == null || message.isEmpty) "" else message + ": ") +