src/Pure/General/timing.scala
changeset 56691 ad5d7461b370
parent 55618 995162143ef4
child 56782 433cf57550fa
--- 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 + ": ") +