diff -r 3e08311ada8e -r 5c4800f6b25a src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Jul 06 16:52:48 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Jul 08 14:43:02 2020 +0200
@@ -575,6 +575,7 @@
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
+  object Session_Timing extends Properties_Function("session_timing")
   object ML_Statistics extends Properties_Function("ML_statistics")
   object Task_Statistics extends Properties_Function("task_statistics")