src/Pure/General/timing.scala

--- a/src/Pure/General/timing.scala	Mon Nov 28 18:08:07 2011 +0100
+++ b/src/Pure/General/timing.scala	Mon Nov 28 20:31:53 2011 +0100
@@ -6,6 +6,7 @@
 
 package isabelle
 
+
 object Time
 {
   def seconds(s: Double): Time = new Time((s * 1000.0) round)
@@ -24,6 +25,21 @@
   def message: String = toString + "s"
 }
 
+
+object Timing
+{
+  def timeit[A](message: String)(e: => A) =
+  {
+    val start = java.lang.System.currentTimeMillis()
+    val result = Exn.capture(e)
+    val stop = java.lang.System.currentTimeMillis()
+    java.lang.System.err.println(
+      (if (message == null || message.isEmpty) "" else message + ": ") +
+        Time.ms(stop - start).message + " elapsed time")
+    Exn.release(result)
+  }
+}
+
 class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
 {
   def message: String =