--- a/src/Pure/Thy/sessions.scala Thu Jun 15 21:26:31 2023 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Jun 15 22:09:56 2023 +0200
@@ -1513,12 +1513,12 @@
port = options.int("build_database_ssh_port"))),
ssh_close = true)
- val build_database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
+ def open_build_database(path: Path): SQL.Database =
+ if (build_database_server) open_database_server()
+ else SQLite.open_database(path, restrict = true)
- def open_build_database(): Option[SQL.Database] =
- if (!build_database_test) None
- else if (build_database_server) Some(open_database_server())
- else Some(SQLite.open_database(build_database, restrict = true))
+ def maybe_open_build_database(path: Path): Option[SQL.Database] =
+ if (!build_database_test) None else Some(open_build_database(path))
def try_open_database(
name: String,
--- 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 {