# HG changeset patch
# User wenzelm
# Date 1594413483 -7200
# Node ID 7a53fc156c2b6d3108bc9a8f8a809a83ac3eacc3
# Parent  13890356df788dcc57b2cb3f2eab2aa0bf7cf322
proper session Timing for build_history log file (see 5c4800f6b25a);

diff -r 13890356df78 -r 7a53fc156c2b src/Pure/Admin/build_history.scala
--- 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
diff -r 13890356df78 -r 7a53fc156c2b src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Jul 10 21:58:49 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Jul 10 22:38:03 2020 +0200
@@ -576,6 +576,9 @@
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
+  {
+    val Threads = new Properties.String("threads")
+  }
   object ML_Statistics extends Properties_Function("ML_statistics")
   object Task_Statistics extends Properties_Function("task_statistics")