src/Pure/PIDE/isabelle_markup.scala

--- a/src/Pure/PIDE/isabelle_markup.scala	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Nov 29 21:50:00 2011 +0100
@@ -168,6 +168,32 @@
   val LOADED_THEORY = "loaded_theory"
 
 
+  /* timing */
+
+  val TIMING = "timing"
+  val ELAPSED = "elapsed"
+  val CPU = "cpu"
+  val GC = "gc"
+
+  object Timing
+  {
+    def apply(timing: isabelle.Timing): Markup =
+      Markup(TIMING, List(
+        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
+        (CPU, Properties.Value.Double(timing.cpu.seconds)),
+        (GC, Properties.Value.Double(timing.gc.seconds))))
+    def unapply(markup: Markup): Option[isabelle.Timing] =
+      markup match {
+        case Markup(TIMING, List(
+          (ELAPSED, Properties.Value.Double(elapsed)),
+          (CPU, Properties.Value.Double(cpu)),
+          (GC, Properties.Value.Double(gc)))) =>
+            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
+        case _ => None
+      }
+  }
+
+
   /* toplevel */
 
   val SUBGOALS = "subgoals"