# HG changeset patch
# User wenzelm
# Date 1594473802 -7200
# Node ID c81e58a81b8c68428d3fce58c7efd806269728c4
# Parent  0b1c830ebf3a27fa719807cc9a7a35f54eb2dbec
clarified inlined protocol messages;

diff -r 0b1c830ebf3a -r c81e58a81b8c src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Jul 11 14:44:50 2020 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Jul 11 15:23:22 2020 +0200
@@ -644,7 +644,7 @@
     task_statistics: Boolean): Session_Info =
   {
     Session_Info(
-      session_timing = log_file.find_props(Protocol.Timing_Marker) getOrElse Nil,
+      session_timing = log_file.find_props(Protocol.Session_Timing_Marker) getOrElse Nil,
       command_timings =
         if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil,
       theory_timings =
diff -r 0b1c830ebf3a -r c81e58a81b8c src/Pure/PIDE/protocol.scala
--- 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")
diff -r 0b1c830ebf3a -r c81e58a81b8c src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Jul 11 14:44:50 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sat Jul 11 15:23:22 2020 +0200
@@ -90,10 +90,8 @@
             | NONE => ())
           else ()
         end
-      else if function = Markup.theory_timing then
+      else if function = Markup.theory_timing orelse function = Markup.session_timing then
         Protocol_Message.marker (#2 function) args
-      else if function = Markup.session_timing then
-        Protocol_Message.marker "Timing" args
       else
         (case Markup.dest_loading_theory props of
           SOME name => Protocol_Message.marker_text "loading_theory" name
diff -r 0b1c830ebf3a -r c81e58a81b8c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 11 14:44:50 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 11 15:23:22 2020 +0200
@@ -364,7 +364,7 @@
               Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
-            session_timings.toList.map(Protocol.Timing_Marker.apply) :::
+            session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)