permissive theory_timings for historic versions;
authorwenzelm
Tue, 17 Oct 2017 11:29:14 +0200
changeset 66875 f60d3e6d5975
parent 66874 0b8da0fc9563
child 66876 b540a5a64a31
permissive theory_timings for historic versions;
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)
           })