src/Pure/Tools/build.scala
changeset 68216 c0f86aee29db
parent 68214 b0e2a19df95b
child 68217 3e90b88b0fc2
     1.1 --- a/src/Pure/Tools/build.scala	Sat May 19 11:57:41 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat May 19 14:12:44 2018 +0200
     1.3 @@ -421,7 +421,7 @@
     1.4            deps0.sessions_structure.build_topological_order.flatMap(name =>
     1.5              store.try_open_database(name) match {
     1.6                case Some(db) =>
     1.7 -                (try { store.read_build(db, name) } finally { db.close }) match {
     1.8 +                using(db)(store.read_build(_, name)) match {
     1.9                    case Some(build)
    1.10                    if build.ok && build.sources == sources_stamp(deps0, name) => None
    1.11                    case _ => Some(name)
    1.12 @@ -594,21 +594,19 @@
    1.13                  {
    1.14                    store.try_open_database(name) match {
    1.15                      case Some(db) =>
    1.16 -                      try {
    1.17 -                        store.read_build(db, name) match {
    1.18 -                          case Some(build) =>
    1.19 -                            val heap_digest = store.find_heap_digest(name)
    1.20 -                            val current =
    1.21 -                              !fresh_build &&
    1.22 -                              build.ok &&
    1.23 -                              build.sources == sources_stamp(deps, name) &&
    1.24 -                              build.input_heaps == ancestor_heaps &&
    1.25 -                              build.output_heap == heap_digest &&
    1.26 -                              !(do_output && heap_digest.isEmpty)
    1.27 -                            (current, heap_digest)
    1.28 -                          case None => (false, None)
    1.29 -                        }
    1.30 -                      } finally { db.close }
    1.31 +                      using(db)(store.read_build(_, name)) match {
    1.32 +                        case Some(build) =>
    1.33 +                          val heap_digest = store.find_heap_digest(name)
    1.34 +                          val current =
    1.35 +                            !fresh_build &&
    1.36 +                            build.ok &&
    1.37 +                            build.sources == sources_stamp(deps, name) &&
    1.38 +                            build.input_heaps == ancestor_heaps &&
    1.39 +                            build.output_heap == heap_digest &&
    1.40 +                            !(do_output && heap_digest.isEmpty)
    1.41 +                          (current, heap_digest)
    1.42 +                        case None => (false, None)
    1.43 +                      }
    1.44                      case None => (false, None)
    1.45                    }
    1.46                  }
    1.47 @@ -626,7 +624,7 @@
    1.48                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.49  
    1.50                    cleanup(name)
    1.51 -                  using(store.open_output_database(name))(db => store.init_session_info(db, name))
    1.52 +                  using(store.open_output_database(name))(store.init_session_info(_, name))
    1.53  
    1.54                    val numa_node = numa_nodes.next(used_node(_))
    1.55                    val job =