# HG changeset patch
# User wenzelm
# Date 1687778412 -7200
# Node ID a40ae2df39ad9a6f7ed2614bec5137a5622a0f80
# Parent  0aa5360fa88bec1a3e1edd00be21d76b2a564afe
clarified database for heaps: do not depend on build_database_test;

diff -r 0aa5360fa88b -r a40ae2df39ad src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Mon Jun 26 13:01:58 2023 +0200
+++ b/src/Pure/Thy/store.scala	Mon Jun 26 13:20:12 2023 +0200
@@ -266,6 +266,9 @@
             port = options.int("build_database_ssh_port"))),
       ssh_close = true)
 
+  def maybe_open_database_server(): Option[SQL.Database] =
+    if (build_database_server) Some(open_database_server()) else None
+
   def open_build_database(path: Path): SQL.Database =
     if (build_database_server) open_database_server()
     else SQLite.open_database(path, restrict = true)
@@ -273,9 +276,6 @@
   def maybe_open_build_database(path: Path): Option[SQL.Database] =
     if (build_database_test) Some(open_build_database(path)) else None
 
-  def maybe_open_heaps_database(): Option[SQL.Database] =
-    if (build_database_test && build_database_server) Some(open_database_server()) else None
-
   def try_open_database(
     name: String,
     output: Boolean = false,
@@ -316,7 +316,7 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
-    using_optional(maybe_open_heaps_database()) { database =>
+    using_optional(maybe_open_database_server()) { database =>
       database.foreach(ML_Heap.clean_entry(_, name))
     }
 
diff -r 0aa5360fa88b -r a40ae2df39ad src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Jun 26 13:01:58 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Mon Jun 26 13:20:12 2023 +0200
@@ -454,7 +454,7 @@
           if (process_result.ok && store_heap && heap.is_file) {
             val slice = Space.MiB(options.real("build_database_slice")).bytes
             val digest =
-              using_optional(store.maybe_open_heaps_database())(
+              using_optional(store.maybe_open_database_server())(
                 ML_Heap.store(_, session_name, heap, slice))
             SHA1.shasum(digest, session_name)
           }
diff -r 0aa5360fa88b -r a40ae2df39ad src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Jun 26 13:01:58 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Mon Jun 26 13:20:12 2023 +0200
@@ -906,7 +906,7 @@
     val cancelled = progress.stopped || !ancestor_results.forall(_.ok)
 
     if (!skipped && !cancelled) {
-      using_optional(store.maybe_open_heaps_database())(
+      using_optional(store.maybe_open_database_server())(
         ML_Heap.restore(_, session_name, store.output_heap(session_name),
           cache = store.cache.compress))
     }