# HG changeset patch
# User wenzelm
# Date 1508232554 -7200
# Node ID f60d3e6d597576b8ae306a3c075d95ba8b0eb31c
# Parent  0b8da0fc95636b409e402e5206dd1696ab54edc1
permissive theory_timings for historic versions;

diff -r 0b8da0fc9563 -r f60d3e6d5975 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Mon Oct 16 19:59:18 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Oct 17 11:29:14 2017 +0200
@@ -260,8 +260,12 @@
             val database = isabelle_output + store.database(session_name)
 
             val properties =
-              using(SQLite.open_database(database))(db =>
-                store.read_theory_timings(db, session_name))
+              if (database.is_file) {
+                using(SQLite.open_database(database))(db =>
+                  try { store.read_theory_timings(db, session_name) }
+                  catch { case ERROR(_) => Nil })
+              }
+              else Nil
 
             properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
           })