src/Pure/library.scala
changeset 45664 ac6e704dcd12
parent 45249 b769a3a370ad
child 45667 546d78f0d81f
--- a/src/Pure/library.scala	Mon Nov 28 18:08:07 2011 +0100
+++ b/src/Pure/library.scala	Mon Nov 28 20:31:53 2011 +0100
@@ -208,20 +208,6 @@
     selection.index = 3
     prototypeDisplayValue = Some("00000%")
   }
-
-
-  /* timing */
-
-  def timeit[A](message: String)(e: => A) =
-  {
-    val start = System.currentTimeMillis()
-    val result = Exn.capture(e)
-    val stop = System.currentTimeMillis()
-    System.err.println(
-      (if (message == null || message.isEmpty) "" else message + ": ") +
-        Time.ms(stop - start).message + " elapsed time")
-    Exn.release(result)
-  }
 }