diff -r 1b97502461a3 -r 8fbe3b3d665b src/Pure/Tools/build_process.scala --- 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 {