# HG changeset patch
# User wenzelm
# Date 1526670310 -7200
# Node ID 5a59fded83c7ebaeb5b9285bf6406161357d61e9
# Parent  1e7defef8c8abcfe488e6ff08de363cdbd690923
clarified heap vs. database operations: discontinued correlation of directory;

diff -r 1e7defef8c8a -r 5a59fded83c7 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri May 18 21:00:15 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri May 18 21:05:10 2018 +0200
@@ -1019,21 +1019,26 @@
         output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
       }
 
-    def find_database_heap(name: String): Option[(Path, Option[String])] =
-      input_dirs.find(dir => (dir + database(name)).is_file).map(dir =>
-        (dir + database(name), read_heap_digest(dir + Path.basic(name))))
+    def find_heap(name: String): Option[Path] =
+      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
+
+    def find_heap_digest(name: String): Option[String] =
+      find_heap(name).flatMap(read_heap_digest(_))
 
     def find_database(name: String): Option[Path] =
       input_dirs.map(_ + database(name)).find(_.is_file)
 
-    def open_database(name: String): SQL.Database =
-      SQLite.open_database(
-        find_database(name) getOrElse error("Missing database for session " + quote(name)))
+    def try_open_database(name: String): Option[SQL.Database] =
+      find_database(name).map(SQLite.open_database(_))
+
+    private def error_input(msg: String): Nothing =
+      error(msg + " -- expected in:\n" + cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
 
     def heap(name: String): Path =
-      input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse
-        error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
-          cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
+      find_heap(name) getOrElse error_input("Missing heap image for session " + quote(name))
+
+    def open_database(name: String): SQL.Database =
+      try_open_database(name) getOrElse error("Missing database file for session " + quote(name))
 
 
     /* session info */
diff -r 1e7defef8c8a -r 5a59fded83c7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri May 18 21:00:15 2018 +0200
+++ b/src/Pure/Tools/build.scala	Fri May 18 21:05:10 2018 +0200
@@ -595,20 +595,23 @@
 
                 val (current, heap_stamp) =
                 {
-                  store.find_database_heap(name) match {
-                    case Some((database, heap_stamp)) =>
-                      using(SQLite.open_database(database))(store.read_build(_, name)) match {
-                        case Some(build) =>
-                          val current =
-                            !fresh_build &&
-                            build.ok &&
-                            build.sources == sources_stamp(deps, name) &&
-                            build.input_heaps == ancestor_heaps &&
-                            build.output_heap == heap_stamp &&
-                            !(do_output && heap_stamp.isEmpty)
-                          (current, heap_stamp)
-                        case None => (false, None)
-                      }
+                  store.try_open_database(name) match {
+                    case Some(db) =>
+                      try {
+                        store.read_build(db, name) match {
+                          case Some(build) =>
+                            val heap_stamp = store.find_heap_digest(name)
+                            val current =
+                              !fresh_build &&
+                              build.ok &&
+                              build.sources == sources_stamp(deps, name) &&
+                              build.input_heaps == ancestor_heaps &&
+                              build.output_heap == heap_stamp &&
+                              !(do_output && heap_stamp.isEmpty)
+                            (current, heap_stamp)
+                          case None => (false, None)
+                        }
+                      } finally { db.close }
                     case None => (false, None)
                   }
                 }