src/Pure/Tools/build_process.scala
changeset 78168 8fbe3b3d665b
parent 78166 70041580b81e
child 78170 c85eeff78b33
--- a/src/Pure/Tools/build_process.scala	Thu Jun 15 21:26:31 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Thu Jun 15 22:09:56 2023 +0200
@@ -122,7 +122,7 @@
       }
 
     def prepare_database(): Unit = {
-      using_option(store.open_build_database()) { db =>
+      using_option(store.maybe_open_build_database(Data.database)) { db =>
         val shared_db = db.is_postgresql
         db.transaction_lock(Data.all_tables, create = true) {
           Data.clean_build(db)
@@ -288,6 +288,8 @@
   /** SQL data model **/
 
   object Data {
+    val database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
+
     def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
       SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body)
 
@@ -839,7 +841,8 @@
 
   /* progress backed by database */
 
-  private val _database: Option[SQL.Database] = store.open_build_database()
+  private val _database: Option[SQL.Database] =
+    store.maybe_open_build_database(Build_Process.Data.database)
 
   protected val (progress, worker_uuid) = synchronized {
     _database match {