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