# HG changeset patch
# User wenzelm
# Date 1526673046 -7200
# Node ID b0e2a19df95b6e42fa5444b2c8a5188348d88348
# Parent  bb93511c7e8f868b15e3c0d3fbb48fe64688c9cf
more abstract database access;

diff -r bb93511c7e8f -r b0e2a19df95b src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri May 18 21:08:24 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri May 18 21:50:46 2018 +0200
@@ -1005,10 +1005,12 @@
 
     def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
 
-    def output_database(name: String): Path = output_dir + database(name)
     def output_log(name: String): Path = output_dir + log(name)
     def output_log_gz(name: String): Path = output_dir + log_gz(name)
 
+    def open_output_database(name: String): SQL.Database =
+      SQLite.open_database(output_dir + database(name))
+
 
     /* input */
 
diff -r bb93511c7e8f -r b0e2a19df95b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri May 18 21:08:24 2018 +0200
+++ b/src/Pure/Tools/build.scala	Fri May 18 21:50:46 2018 +0200
@@ -38,32 +38,29 @@
     {
       val no_timings: Timings = (Nil, 0.0)
 
-      store.find_database(name) match {
+      store.try_open_database(name) match {
         case None => no_timings
-        case Some(database) =>
+        case Some(db) =>
           def ignore_error(msg: String) =
           {
-            progress.echo_warning("Ignoring bad database: " +
-              database.expand + (if (msg == "") "" else "\n" + msg))
+            progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
             no_timings
           }
           try {
-            using(SQLite.open_database(database))(db =>
-            {
-              val command_timings = store.read_command_timings(db, name)
-              val session_timing =
-                store.read_session_timing(db, name) match {
-                  case Markup.Elapsed(t) => t
-                  case _ => 0.0
-                }
-              (command_timings, session_timing)
-            })
+            val command_timings = store.read_command_timings(db, name)
+            val session_timing =
+              store.read_session_timing(db, name) match {
+                case Markup.Elapsed(t) => t
+                case _ => 0.0
+              }
+            (command_timings, session_timing)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
             case _: XML.Error => ignore_error("")
           }
+          finally { db.close }
       }
     }
 
@@ -195,7 +192,7 @@
     isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
 
     private val export_tmp_dir = Isabelle_System.tmp_dir("export")
-    private val export_consumer = Export.consumer(SQLite.open_database(store.output_database(name)))
+    private val export_consumer = Export.consumer(store.open_output_database(name))
 
     private val future_result: Future[Process_Result] =
       Future.thread("build") {
@@ -422,9 +419,9 @@
       if (soft_build && !fresh_build) {
         val outdated =
           deps0.sessions_structure.build_topological_order.flatMap(name =>
-            store.find_database(name) match {
-              case Some(database) =>
-                using(SQLite.open_database(database))(store.read_build(_, name)) match {
+            store.try_open_database(name) match {
+              case Some(db) =>
+                (try { store.read_build(db, name) } finally { db.close }) match {
                   case Some(build)
                   if build.ok && build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
@@ -560,7 +557,7 @@
                     ml_statistics = true,
                     task_statistics = true)
 
-              using(SQLite.open_database(store.output_database(name)))(db =>
+              using(store.open_output_database(name))(db =>
                 store.write_session_info(db, name,
                   build_log =
                     if (process_result.timeout) build_log.error("Timeout") else build_log,
@@ -629,8 +626,7 @@
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
 
                   cleanup(name)
-                  using(SQLite.open_database(store.output_database(name)))(db =>
-                    store.init_session_info(db, name))
+                  using(store.open_output_database(name))(db => store.init_session_info(db, name))
 
                   val numa_node = numa_nodes.next(used_node(_))
                   val job =