src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Thu Aug 06 23:13:24 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Aug 06 23:27:52 2020 +0200
@@ -576,6 +576,8 @@
       }
   }
 
+  val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
+
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")