--- 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 =
--- 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")
--- 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
--- 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)