diff -r 92e58b76dbb1 -r 3391a493f39a src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Apr 09 15:59:02 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Apr 09 20:16:52 2013 +0200
@@ -193,6 +193,7 @@
   {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
+
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {
         case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
@@ -206,6 +207,7 @@
   object Timing
   {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
+
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
@@ -214,6 +216,22 @@
   }
 
 
+  /* command timing */
+
+  object Command_Timing
+  {
+    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
+      props match {
+        case (FUNCTION, "command_timing") :: args =>
+          (args, args) match {
+            case (Position.Id(id), Timing_Properties(timing)) => Some((id, timing))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
+
   /* toplevel */
 
   val SUBGOALS = "subgoals"