# HG changeset patch
# User wenzelm
# Date 1596749272 -7200
# Node ID 1b06ed2549439c421a89c8ef7eec4906476f65db
# Parent  36743e0e2c4cd5a7e9cf4eeb79b48dcca93c38ff
more compact command_timings, as in former batch-build;

diff -r 36743e0e2c4c -r 1b06ed254943 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Aug 06 23:13:24 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Aug 06 23:27:52 2020 +0200
@@ -576,6 +576,8 @@
       }
   }
 
+  val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
+
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
diff -r 36743e0e2c4c -r 1b06ed254943 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Aug 06 23:13:24 2020 +0200
+++ b/src/Pure/Tools/build.scala	Thu Aug 06 23:27:52 2020 +0200
@@ -299,12 +299,20 @@
                 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))
+
             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, Markup.Command_Timing.unapply),
+                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.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply),