diff -r 6f47c49fed84 -r 2bb7ec08574a src/Pure/General/timing.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/timing.scala	Sat Nov 06 17:55:32 2010 +0100
@@ -0,0 +1,20 @@
+/*  Title:      Pure/General/timing.scala
+    Author:     Makarius
+
+Basic support for time measurement.
+*/
+
+package isabelle
+
+
+sealed case class Timing(val elapsed: Double, cpu: Double, gc: Double)
+{
+  private def print_time(seconds: Double): String =
+    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+
+  def message: String =
+    print_time(elapsed) + "s elapsed time, " +
+    print_time(cpu) + "s cpu time, " +
+    print_time(gc) + "s GC time"
+}
+