--- 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),