# HG changeset patch
# User wenzelm
# Date 1687947609 -7200
# Node ID 2d2417a6331424f5768431ff0efe641828bebbdb
# Parent  5c91541284cd051cda855a45c9df1cf709d37c49
clarified signature: better default;

diff -r 5c91541284cd -r 2d2417a63314 src/Pure/Thy/store.scala
--- 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,
diff -r 5c91541284cd -r 2d2417a63314 src/Pure/Tools/build.scala
--- 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)
       }
diff -r 5c91541284cd -r 2d2417a63314 src/Pure/Tools/build_process.scala
--- 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 {