--- a/src/Pure/System/progress.scala Fri Jun 16 14:01:30 2023 +0200
+++ b/src/Pure/System/progress.scala Fri Jun 16 14:20:18 2023 +0200
@@ -42,6 +42,8 @@
/* SQL data model */
object Data {
+ val database: Path = Path.explode("$ISABELLE_HOME_USER/progress.db")
+
def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
SQL.Table("isabelle_progress" + if_proper(name, "_" + name), columns, body = body)
--- a/src/Pure/Tools/build_process.scala Fri Jun 16 14:01:30 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Fri Jun 16 14:20:18 2023 +0200
@@ -848,9 +848,7 @@
_database match {
case None => (build_progress, UUID.random().toString)
case Some(db) =>
- val progress_db =
- if (db.is_postgresql) store.open_database_server()
- else db
+ val progress_db = store.open_build_database(Progress.Data.database)
val progress =
new Database_Progress(progress_db, build_progress,
hostname = hostname,