# HG changeset patch
# User wenzelm
# Date 1526731964 -7200
# Node ID c0f86aee29db78913e9dbbf030dc96a4c869a29c
# Parent  a477f78a936587ceef5bf7287ae53d91489e9f3c
tuned;

diff -r a477f78a9365 -r c0f86aee29db src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat May 19 11:57:41 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat May 19 14:12:44 2018 +0200
@@ -421,7 +421,7 @@
           deps0.sessions_structure.build_topological_order.flatMap(name =>
             store.try_open_database(name) match {
               case Some(db) =>
-                (try { store.read_build(db, name) } finally { db.close }) match {
+                using(db)(store.read_build(_, name)) match {
                   case Some(build)
                   if build.ok && build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
@@ -594,21 +594,19 @@
                 {
                   store.try_open_database(name) match {
                     case Some(db) =>
-                      try {
-                        store.read_build(db, name) match {
-                          case Some(build) =>
-                            val heap_digest = 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_digest &&
-                              !(do_output && heap_digest.isEmpty)
-                            (current, heap_digest)
-                          case None => (false, None)
-                        }
-                      } finally { db.close }
+                      using(db)(store.read_build(_, name)) match {
+                        case Some(build) =>
+                          val heap_digest = 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_digest &&
+                            !(do_output && heap_digest.isEmpty)
+                          (current, heap_digest)
+                        case None => (false, None)
+                      }
                     case None => (false, None)
                   }
                 }
@@ -626,7 +624,7 @@
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
 
                   cleanup(name)
-                  using(store.open_output_database(name))(db => store.init_session_info(db, name))
+                  using(store.open_output_database(name))(store.init_session_info(_, name))
 
                   val numa_node = numa_nodes.next(used_node(_))
                   val job =