src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Mon Apr 29 14:07:03 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Apr 29 15:47:42 2013 +0200
@@ -218,18 +218,7 @@
 
   /* 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
-      }
-  }
+  val COMMAND_TIMING = "command_timing"
 
 
   /* toplevel */