src/Pure/PIDE/markup.ML

   val cancel_scala: string -> Properties.T
   val ML_statistics: Properties.entry
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
+  val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val build_session_finished: Properties.T
   val print_operationsN: string
   val print_operations: Properties.T

 
 val command_timing = (functionN, "command_timing");
 
 val theory_timing = (functionN, "theory_timing");
 
+val session_timing = (functionN, "session_timing");
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   | dest_loading_theory _ = NONE;