clarified command_timings protocol;

--- a/src/Pure/PIDE/markup.scala	Wed Nov 25 17:49:09 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Nov 25 20:48:33 2020 +0100
@@ -589,6 +589,7 @@
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
+  def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")

--- a/src/Pure/Tools/build_job.scala	Wed Nov 25 17:49:09 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Nov 25 20:48:33 2020 +0100
@@ -132,25 +132,26 @@
               case _ => false
             }
 
-          private def command_timing(props: Properties.T): Option[Properties.T] =
-            for {
-              props1 <- Markup.Command_Timing.unapply(props)
-              elapsed <- Markup.Elapsed.unapply(props1)
-              elapsed_time = Time.seconds(elapsed)
-              if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
-            } yield props1.filter(p => Markup.command_timing_properties(p._1))
-
           override val functions =
             List(
               Markup.Build_Session_Finished.name -> build_session_finished,
               Markup.Loading_Theory.name -> loading_theory,
               Markup.EXPORT -> export,
-              fun(Markup.Command_Timing.name, command_timings, command_timing),
               fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
               fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
               fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
         })
 
+      session.command_timings += Session.Consumer("command_timings")
+        {
+          case Session.Command_Timing(props) =>
+            for {
+              elapsed <- Markup.Elapsed.unapply(props)
+              elapsed_time = Time.seconds(elapsed)
+              if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
+            } command_timings += props.filter(Markup.command_timing_property)
+        }
+
       session.runtime_statistics += Session.Consumer("ML_statistics")
         {
           case Session.Runtime_Statistics(props) => runtime_statistics += props