src/Pure/library.scala
changeset 41119 8662b9b1f123
parent 40744 8a57ff2c2600
child 44313 e1fff67b23ac
equal deleted inserted replaced
41095:df8c7dc30214 41119:8662b9b1f123
   135 
   135 
   136   /* timing */
   136   /* timing */
   137 
   137 
   138   def timeit[A](message: String)(e: => A) =
   138   def timeit[A](message: String)(e: => A) =
   139   {
   139   {
   140     val start = System.nanoTime()
   140     val start = System.currentTimeMillis()
   141     val result = Exn.capture(e)
   141     val result = Exn.capture(e)
   142     val stop = System.nanoTime()
   142     val stop = System.currentTimeMillis()
   143     System.err.println(
   143     System.err.println(
   144       (if (message == null || message.isEmpty) "" else message + ": ") +
   144       (if (message == null || message.isEmpty) "" else message + ": ") +
   145         ((stop - start).toDouble / 1000000) + "ms elapsed time")
   145         new Time(stop - start).message + " elapsed time")
   146     Exn.release(result)
   146     Exn.release(result)
   147   }
   147   }
   148 }
   148 }