src/Pure/PIDE/markup.scala

         case _ => None
       }
   }
 
 
-  /* command timing */
-
-  val COMMAND_TIMING = "command_timing"
+  /* protocol functions */
+
+  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
+
+  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
 
 
   /* command indentation */
 
   object Command_Indent