--- a/src/Pure/PIDE/protocol.scala Sat Jul 11 14:44:50 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala Sat Jul 11 15:23:22 2020 +0200
@@ -14,9 +14,9 @@
val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
val Export_Marker = Protocol_Message.Marker("export")
val Meta_Info_Marker = Protocol_Message.Marker("meta_info")
- val Timing_Marker = Protocol_Message.Marker("Timing")
val Command_Timing_Marker = Protocol_Message.Marker("command_timing")
val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing")
+ val Session_Timing_Marker = Protocol_Message.Marker("session_timing")
val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics")
val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics")
val Error_Message_Marker = Protocol_Message.Marker("error_message")