--- a/src/Pure/Thy/store.scala Wed Jun 28 12:16:02 2023 +0200
+++ b/src/Pure/Thy/store.scala Wed Jun 28 12:20:09 2023 +0200
@@ -274,8 +274,9 @@
if (build_database_server) open_database_server()
else SQLite.open_database(path, restrict = true)
- def maybe_open_build_database(path: Path): Option[SQL.Database] =
- if (build_database_test) Some(open_build_database(path)) else None
+ def maybe_open_build_database(
+ path: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
+ ): Option[SQL.Database] = if (build_database_test) Some(open_build_database(path)) else None
def try_open_database(
name: String,
--- a/src/Pure/Tools/build.scala Wed Jun 28 12:16:02 2023 +0200
+++ b/src/Pure/Tools/build.scala Wed Jun 28 12:20:09 2023 +0200
@@ -382,11 +382,11 @@
/* identified builds */
def read_builds(options: Options): List[Build_Process.Build] =
- using_option(Store(options).maybe_open_build_database(Build_Process.Data.database))(
+ using_option(Store(options).maybe_open_build_database())(
Build_Process.read_builds).getOrElse(Nil).filter(_.active)
def print_builds(options: Options, builds: List[Build_Process.Build]): String =
- using_optional(Store(options).maybe_open_build_database(Build_Process.Data.database)) { build_database =>
+ using_optional(Store(options).maybe_open_build_database()) { build_database =>
val print_database =
build_database match {
case None => ""
@@ -433,7 +433,7 @@
val build_options = store.options
val sessions =
- using_optional(store.maybe_open_build_database(Build_Process.Data.database)) {
+ using_optional(store.maybe_open_build_database()) {
case None => error("Cannot access build database")
case Some(db) => Build_Process.read_sessions(db, build_master.build_uuid)
}
--- a/src/Pure/Tools/build_process.scala Wed Jun 28 12:16:02 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Wed Jun 28 12:20:09 2023 +0200
@@ -82,7 +82,7 @@
Isabelle_System.make_directory(store.output_dir + Path.basic("log"))
- using_option(store.maybe_open_build_database(Data.database)) { db =>
+ using_option(store.maybe_open_build_database()) { db =>
val shared_db = db.is_postgresql
Data.transaction_lock(db, create = true) {
Data.clean_build(db)
@@ -825,11 +825,11 @@
catch { case exn: Throwable => close(); throw exn }
private val _build_database: Option[SQL.Database] =
- try { store.maybe_open_build_database(Build_Process.Data.database) }
+ try { store.maybe_open_build_database() }
catch { case exn: Throwable => close(); throw exn }
private val _host_database: Option[SQL.Database] =
- try { store.maybe_open_build_database(Host.Data.database) }
+ try { store.maybe_open_build_database(path = Host.Data.database) }
catch { case exn: Throwable => close(); throw exn }
protected val (progress, worker_uuid) = synchronized {