# HG changeset patch
# User wenzelm
# Date 1678024412 -3600
# Node ID acaa89cb977bf8bbc981550e889517319585cf3a
# Parent  43bfb65ee9b30115a36633b762335a54c1ef5837
tuned signature;

diff -r 43bfb65ee9b3 -r acaa89cb977b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Mar 05 13:42:10 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Mar 05 14:53:32 2023 +0100
@@ -116,6 +116,16 @@
         case None => Nil
       }
 
+    def open_database(): Option[SQL.Database] =
+      if (!build_options.bool("build_database_test")) None
+      else if (store.database_server) Some(store.open_database_server())
+      else {
+        val db = SQLite.open_database(Build_Process.Data.database)
+        try { Isabelle_System.chmod("600", Build_Process.Data.database) }
+        catch { case exn: Throwable => db.close(); throw exn }
+        Some(db)
+      }
+
     def store_heap(name: String): Boolean =
       build_heap || Sessions.is_pure(name) ||
       sessions.valuesIterator.exists(_.ancestors.contains(name))
@@ -605,15 +615,7 @@
 
   private var _state: Build_Process.State = init_state(Build_Process.State())
 
-  private val _database: Option[SQL.Database] =
-    if (!build_options.bool("build_database_test")) None
-    else if (store.database_server) Some(store.open_database_server())
-    else {
-      val db = SQLite.open_database(Build_Process.Data.database)
-      try { Isabelle_System.chmod("600", Build_Process.Data.database) }
-      catch { case exn: Throwable => db.close(); throw exn }
-      Some(db)
-    }
+  private val _database: Option[SQL.Database] = build_context.open_database()
 
   def close(): Unit = synchronized { _database.foreach(_.close()) }