# HG changeset patch
# User wenzelm
# Date 1606429399 -3600
# Node ID a4d7da18ac5cd8172f7fb62f392d6ee604fcdaa5
# Parent  98fe7a10ace3c9002b4f8eea7d0983e9093e18f5
store timings for used_theories in canonical order, with reconstructed store.read_theories;

diff -r 98fe7a10ace3 -r a4d7da18ac5c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Nov 26 20:49:40 2020 +0000
+++ b/src/Pure/Thy/sessions.scala	Thu Nov 26 23:23:19 2020 +0100
@@ -1465,6 +1465,9 @@
     def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.task_statistics)
 
+    def read_theories(db: SQL.Database, name: String): List[String] =
+      read_theory_timings(db, name).flatMap(Markup.Name.unapply)
+
     def read_errors(db: SQL.Database, name: String): List[String] =
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = xz_cache)
 
diff -r 98fe7a10ace3 -r a4d7da18ac5c src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Nov 26 20:49:40 2020 +0000
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 26 23:23:19 2020 +0100
@@ -265,12 +265,19 @@
 
       val result =
       {
+        val theory_timing =
+          theory_timings.iterator.map(
+            { case props @ Markup.Name(name) => name -> props }).toMap
+        val used_theory_timings =
+          for { (name, _) <- deps(session_name).used_theories }
+            yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
+
         val more_output =
           Library.trim_line(stdout.toString) ::
             messages.toList.map(message =>
               Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
-            theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
+            used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
             session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::