# HG changeset patch
# User wenzelm
# Date 1594475574 -7200
# Node ID 2550bac18b491e9c75beb64889d0af17f97c6dd0
# Parent  6a24ecc4ff1b740db535e87ac3ed656685364b3d
tuned;

diff -r 6a24ecc4ff1b -r 2550bac18b49 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jul 11 15:51:15 2020 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Jul 11 15:52:54 2020 +0200
@@ -284,6 +284,13 @@
             if (database.is_file) {
               using(SQLite.open_database(database))(db =>
               {
+                val theory_timings =
+                  try {
+                    store.read_theory_timings(db, session_name).map(ps =>
+                      Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
+                  }
+                  catch { case ERROR(_) => Nil }
+
                 val session_timing =
                 {
                   val props = store.read_session_timing(db, session_name)
@@ -292,13 +299,6 @@
                     Markup.Timing_Properties.parse(props))
                 }
 
-                val theory_timings =
-                  try {
-                    store.read_theory_timings(db, session_name).map(ps =>
-                      Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
-                  }
-                  catch { case ERROR(_) => Nil }
-
                 val session_sources =
                   store.read_build(db, session_name).map(_.sources) match {
                     case Some(sources) if sources.length == SHA1.digest_length =>
@@ -306,7 +306,7 @@
                     case _ => Nil
                   }
 
-                session_timing :: theory_timings ::: session_sources
+                theory_timings ::: List(session_timing) ::: session_sources
               })
             }
             else Nil