# HG changeset patch
# User wenzelm
# Date 1278182190 -7200
# Node ID bb27d99a9a693f3e795f2aaac5ae667b64c33b7c
# Parent  305c326db33ba53945d5786b00007854763cdf1c
more precise timing;

diff -r 305c326db33b -r bb27d99a9a69 src/Pure/library.scala
--- a/src/Pure/library.scala	Sat Jul 03 20:20:13 2010 +0200
+++ b/src/Pure/library.scala	Sat Jul 03 20:36:30 2010 +0200
@@ -129,11 +129,12 @@
 
   def timeit[A](message: String)(e: => A) =
   {
-    val start = System.currentTimeMillis()
+    val start = System.nanoTime()
     val result = Exn.capture(e)
-    val stop = System.currentTimeMillis()
+    val stop = System.nanoTime()
     System.err.println(
-      (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
+      (if (message == null || message.isEmpty) "" else message + ": ") +
+        ((stop - start).toDouble / 1000000) + "ms elapsed time")
     Exn.release(result)
   }
 }