clarified signature;

--- a/src/Pure/Build/build_job.scala	Tue Apr 16 15:14:55 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Apr 16 16:27:40 2024 +0200
@@ -31,12 +31,9 @@
     server: SSH.Server = SSH.no_server,
     progress: Progress = new Progress
   ): Unit = {
-    using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
-      heaps_database =>
-        for (db <- database_server orElse heaps_database) {
-          val slice = Space.MiB(options.real("build_database_slice"))
-          ML_Heap.store(db, session, slice, cache = store.cache.compress, progress = progress)
-        }
+    store.maybe_using_heaps_database(database_server, server = server) { db =>
+      val slice = Space.MiB(options.real("build_database_slice"))
+      ML_Heap.store(db, session, slice, cache = store.cache.compress, progress = progress)
     }
   }
 

--- a/src/Pure/Build/store.scala	Tue Apr 16 15:14:55 2024 +0200
+++ b/src/Pure/Build/store.scala	Tue Apr 16 16:27:40 2024 +0200
@@ -386,6 +386,15 @@
     else store.maybe_open_database_server(server = server, guard = build_cluster)
   }
 
+  def maybe_using_heaps_database[A](
+    database_server: Option[SQL.Database],
+    server: SSH.Server = SSH.no_server
+  )(f: SQL.Database => A): Option[A] = {
+    using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
+      heaps_database => (database_server orElse heaps_database).map(f)
+    }
+  }
+
   def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database =
     if (build_database_server || build_cluster) open_database_server(server = server)
     else SQLite.open_database(path, restrict = true)