src/Pure/PIDE/protocol.scala

--- a/src/Pure/PIDE/protocol.scala	Mon Apr 29 14:07:03 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Apr 29 15:47:42 2013 +0200
@@ -84,6 +84,22 @@
     (Status.init /: markups)(command_status(_, _))
 
 
+  /* command timing */
+
+  object Command_Timing
+  {
+    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
+      props match {
+        case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
+          (args, args) match {
+            case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
+
   /* node status */
 
   sealed case class Node_Status(