src/Pure/PIDE/protocol.scala
changeset 72012 c81e58a81b8c
parent 71875 aaa984499d36
child 72234 4d615ec4b6b1
--- 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")