1.1 --- a/src/Pure/library.scala	Sat Jul 03 20:20:13 2010 +0200
     1.2 +++ b/src/Pure/library.scala	Sat Jul 03 20:36:30 2010 +0200
     1.3 @@ -129,11 +129,12 @@
     1.4  
     1.5    def timeit[A](message: String)(e: => A) =
     1.6    {
     1.7 -    val start = System.currentTimeMillis()
     1.8 +    val start = System.nanoTime()
     1.9      val result = Exn.capture(e)
    1.10 -    val stop = System.currentTimeMillis()
    1.11 +    val stop = System.nanoTime()
    1.12      System.err.println(
    1.13 -      (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
    1.14 +      (if (message == null || message.isEmpty) "" else message + ": ") +
    1.15 +        ((stop - start).toDouble / 1000000) + "ms elapsed time")
    1.16      Exn.release(result)
    1.17    }
    1.18  }