# HG changeset patch
# User wenzelm
# Date 1263238619 -3600
# Node ID f799f374959664e608074c647e190c712b3f12ac
# Parent  2f890016afabfdd8b195a14214d09d10c89abcac
timeit message;

diff -r 2f890016afab -r f799f3749596 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Jan 11 20:36:31 2010 +0100
+++ b/src/Pure/library.scala	Mon Jan 11 20:36:59 2010 +0100
@@ -55,12 +55,13 @@
 
   /* timing */
 
-  def timeit[A](e: => A) =
+  def timeit[A](message: String)(e: => A) =
   {
     val start = System.currentTimeMillis()
     val result = Exn.capture(e)
     val stop = System.currentTimeMillis()
-    System.err.println((stop - start) + "ms elapsed time")
+    System.err.println(
+      (if (message.isEmpty) "" else message + " ") + (stop - start) + "ms elapsed time")
     Exn.release(result)
   }
 }