--- a/src/Pure/Admin/build_history.scala Fri Jul 10 21:58:49 2020 +0200
+++ b/src/Pure/Admin/build_history.scala Fri Jul 10 22:38:03 2020 +0200
@@ -284,6 +284,14 @@
if (database.is_file) {
using(SQLite.open_database(database))(db =>
{
+ val session_timing =
+ {
+ val props = store.read_session_timing(db, session_name)
+ val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse "1"
+ val timing = Markup.Timing_Properties.unapply(props) getOrElse Timing.zero
+ "Timing " + session_name + " (" + threads + " threads, " + timing.message_resources + ")"
+ }
+
val theory_timings =
try {
store.read_theory_timings(db, session_name).map(ps =>
@@ -298,7 +306,7 @@
case _ => Nil
}
- theory_timings ::: session_sources
+ session_timing :: theory_timings ::: session_sources
})
}
else Nil