# HG changeset patch
# User wenzelm
# Date 1489780640 -3600
# Node ID a53a5ae88205be7690aed8782b9d00b82f563c44
# Parent  e3bd1e7ddd23f981c256c5fd5ca05da678c2049a
prefer database, but also accept log.gz from historic versions;

diff -r e3bd1e7ddd23 -r a53a5ae88205 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Fri Mar 17 20:33:27 2017 +0100
+++ b/src/Pure/Admin/build_history.scala	Fri Mar 17 20:57:20 2017 +0100
@@ -207,6 +207,8 @@
 
       /* output log */
 
+      val store = Sessions.store()
+
       val meta_info =
         Build_Log.Prop.multiple(Build_Log.Prop.build_tags, build_tags) :::
         Build_Log.Prop.multiple(Build_Log.Prop.build_args, build_args1) :::
@@ -222,12 +224,21 @@
       val ml_statistics =
         build_info.finished_sessions.flatMap(session_name =>
           {
-            val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
-            if (session_log.is_file) {
-              Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
-                ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
-            }
-            else Nil
+            val database = isabelle_output + store.database(session_name)
+            val log_gz = isabelle_output + store.log_gz(session_name)
+
+            val properties =
+              if (database.is_file) {
+                using(SQLite.open_database(database))(db =>
+                  Sessions.Session_Info.read_build_log(
+                    store, db, session_name, ml_statistics = true)).ml_statistics
+              }
+              else if (log_gz.is_file) {
+                Build_Log.Log_File(log_gz).
+                  parse_session_info(session_name, ml_statistics = true).ml_statistics
+              }
+              else Nil
+            properties.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
           })
 
       val heap_sizes =