# HG changeset patch
# User wenzelm
# Date 1687524195 -7200
# Node ID c268def0784bf209eec3acc5b8e22154f8f66655
# Parent  7ba63bd216afb97b0e8edc9c38943c75c834d883
clarified signature: prefer explicit combinator;

diff -r 7ba63bd216af -r c268def0784b src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Fri Jun 23 13:51:23 2023 +0200
+++ b/src/Pure/ROOT.scala	Fri Jun 23 14:43:15 2023 +0200
@@ -13,6 +13,8 @@
     Library.using(a)(f)
   def using_option[A <: AutoCloseable, B](opt: Option[A])(f: A => B): Option[B] =
     Library.using_option(opt)(f)
+  def using_optional[A <: AutoCloseable, B](opt: Option[A])(f: Option[A] => B): B =
+    Library.using_optional(opt)(f)
 
   val space_explode = Library.space_explode _
   val split_lines = Library.split_lines _
diff -r 7ba63bd216af -r c268def0784b src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Fri Jun 23 13:51:23 2023 +0200
+++ b/src/Pure/Thy/store.scala	Fri Jun 23 14:43:15 2023 +0200
@@ -316,8 +316,8 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
-    for (db <- maybe_open_heaps_database()) {
-      using(db)(ML_Heap.clean_entry(_, name))
+    using_optional(maybe_open_heaps_database()) { database =>
+      database.foreach(ML_Heap.clean_entry(_, name))
     }
 
     if (init) {
diff -r 7ba63bd216af -r c268def0784b src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Jun 23 13:51:23 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Fri Jun 23 14:43:15 2023 +0200
@@ -453,11 +453,8 @@
           val heap = store.output_heap(session_name)
           if (process_result.ok && store_heap && heap.is_file) {
             val slice = Space.MiB(options.real("build_database_slice")).bytes
-            val digest = {
-              val database = store.maybe_open_heaps_database()
-              try { ML_Heap.store(database, heap, slice = slice) }
-              finally { database.foreach(_.close()) }
-            }
+            val digest =
+              using_optional(store.maybe_open_heaps_database())(ML_Heap.store(_, heap, slice))
             SHA1.shasum(digest, session_name)
           }
           else SHA1.no_shasum
diff -r 7ba63bd216af -r c268def0784b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Jun 23 13:51:23 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jun 23 14:43:15 2023 +0200
@@ -906,13 +906,10 @@
     val cancelled = progress.stopped || !ancestor_results.forall(_.ok)
 
     if (!skipped && !cancelled) {
-      val database = store.maybe_open_heaps_database()
-      try {
-        for (db <- database) {
-          ML_Heap.restore(db, store.output_heap(session_name), cache = store.cache.compress)
-        }
+      using_optional(store.maybe_open_heaps_database()) { database =>
+        database.foreach(
+          ML_Heap.restore(_, store.output_heap(session_name), cache = store.cache.compress))
       }
-      finally { database.foreach(_.close()) }
     }
 
     val result_name = (session_name, worker_uuid, build_uuid)
diff -r 7ba63bd216af -r c268def0784b src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Jun 23 13:51:23 2023 +0200
+++ b/src/Pure/library.scala	Fri Jun 23 14:43:15 2023 +0200
@@ -23,6 +23,16 @@
   def using_option[A <: AutoCloseable, B](opt: Option[A])(f: A => B): Option[B] =
     opt.map(a => using(a)(f))
 
+  def using_optional[A <: AutoCloseable, B](opt: Option[A])(f: Option[A] => B): B = {
+    try { f(opt) }
+    finally {
+      opt match {
+        case Some(a) if a != null => a.close()
+        case _ =>
+      }
+    }
+  }
+
 
   /* integers */