--- 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)
- }
}