# HG changeset patch
# User wenzelm
# Date 1688732458 -7200
# Node ID c8fde312c895748a4d9c8ee8bba7be17a97a49aa
# Parent  8c999990262ce20b0355efd4e6546418af13fe3c
clarified signature: ensure disjoint data spaces;

diff -r 8c999990262c -r c8fde312c895 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Jul 07 14:17:53 2023 +0200
+++ b/src/Pure/General/sql.scala	Fri Jul 07 14:20:58 2023 +0200
@@ -252,11 +252,10 @@
 
     def transaction_lock[A](
       db: Database,
-      more_tables: Tables = Tables.empty,
       create: Boolean = false,
       synchronized: Boolean = false,
     )(body: => A): A = {
-      def run: A = db.transaction { (tables ::: more_tables).lock(db, create = create); body }
+      def run: A = db.transaction { tables.lock(db, create = create); body }
       if (synchronized) db.synchronized { run } else run
     }
 
diff -r 8c999990262c -r c8fde312c895 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Jul 07 14:17:53 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jul 07 14:20:58 2023 +0200
@@ -845,12 +845,12 @@
   private val _build_database: Option[SQL.Database] =
     try {
       for (db <- store.maybe_open_build_database()) yield {
-        val more_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty
+        val store_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty
         Build_Process.Data.transaction_lock(db, create = true) {
           Build_Process.Data.clean_build(db)
-          more_tables.lock(db, create = true)
+          store_tables.lock(db, create = true)
         }
-        db.vacuum(Build_Process.Data.tables ::: more_tables)
+        db.vacuum(Build_Process.Data.tables ::: store_tables)
         db
       }
     }