# HG changeset patch
# User wenzelm
# Date 1686918018 -7200
# Node ID c85eeff78b33e2e188388ba7988c8b5928a5a3f1
# Parent  5ad1ae8626de658bf5728b516bd28f6cc725594d
proper support for SQLite: avoid conflicts on transaction_lock;

diff -r 5ad1ae8626de -r c85eeff78b33 src/Pure/System/progress.scala
--- 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)
 
diff -r 5ad1ae8626de -r c85eeff78b33 src/Pure/Tools/build_process.scala
--- 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,