proper support for SQLite: avoid conflicts on transaction_lock;
authorwenzelm
Fri, 16 Jun 2023 14:20:18 +0200
changeset 78170 c85eeff78b33
parent 78169 5ad1ae8626de
child 78171 412a24a4c751
proper support for SQLite: avoid conflicts on transaction_lock;
src/Pure/System/progress.scala
src/Pure/Tools/build_process.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)
 
--- 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,