# HG changeset patch
# User wenzelm
# Date 1678359320 -3600
# Node ID dd8b08729458cdc96b7ab2de350c98cbc74458ac
# Parent  4e4aaec82be4577b1af70f3995b04e39885cf877
clarified signature;

diff -r 4e4aaec82be4 -r dd8b08729458 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Mar 08 22:43:04 2023 +0100
+++ b/src/Pure/General/sql.scala	Thu Mar 09 11:55:20 2023 +0100
@@ -213,6 +213,32 @@
   }
 
 
+  /* table groups */
+
+  object Tables {
+    def list(list: List[Table]): Tables = new Tables(list)
+    def apply(args: Table*): Tables = list(args.toList)
+  }
+
+  final class Tables private(val list: List[Table]) extends Iterable[Table] {
+    override def toString: String = list.mkString("SQL.Tables(", ", ", ")")
+
+    def iterator: Iterator[Table] = list.iterator
+
+    // requires transaction
+    def create_lock(db: Database): Unit = {
+      foreach(db.create_table(_))
+      lock(db)
+    }
+
+    // requires transaction
+    def lock(db: Database): Unit = {
+      val sql = db.lock_tables(list)
+      if (sql.nonEmpty) db.execute_statement(sql)
+    }
+  }
+
+
 
   /** SQL database operations **/
 
@@ -369,7 +395,10 @@
       finally { connection.setAutoCommit(auto_commit) }
     }
 
-    def lock_tables(tables: List[Table]): Unit = {}  // PostgreSQL only
+    def transaction_lock[A](tables: Tables)(body: => A): A =
+      transaction { tables.lock(db); body }
+
+    def lock_tables(tables: List[Table]): Source = ""  // PostgreSQL only
 
 
     /* statements and results */
@@ -559,8 +588,8 @@
     // see https://www.postgresql.org/docs/current/sql-lock.html
     // see https://www.postgresql.org/docs/current/explicit-locking.html
 
-    override def lock_tables(tables: List[SQL.Table]): Unit =
-      execute_statement("LOCK TABLE " + tables.mkString(", ") + " IN ACCESS EXCLUSIVE MODE")
+    override def lock_tables(tables: List[SQL.Table]): PostgreSQL.Source =
+      "LOCK TABLE " + tables.mkString(", ") + " IN ACCESS EXCLUSIVE MODE"
 
 
     /* notifications: IPC via database server */
diff -r 4e4aaec82be4 -r dd8b08729458 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 22:43:04 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 09 11:55:20 2023 +0100
@@ -133,8 +133,7 @@
     def prepare_database(): Unit = {
       using_option(open_database()) { db =>
         db.transaction {
-          for (table <- Data.all_tables) db.create_table(table)
-          db.lock_tables(Data.all_tables)
+          Data.all_tables.create_lock(db)
           Data.clean_build(db)
         }
         db.rebuild()
@@ -722,8 +721,8 @@
 
     /* collective operations */
 
-    def all_tables: List[SQL.Table] =
-      List(
+    val all_tables: SQL.Tables =
+      SQL.Tables(
         Base.table,
         Workers.table,
         Progress.table,
@@ -754,15 +753,6 @@
       stamp_worker(db, worker_uuid, serial)
       state.set_serial(serial).set_workers(read_workers(db))
     }
-
-
-    /* transaction_lock */
-
-    def transaction_lock[A](db: SQL.Database, body: => A): A =
-      db.transaction {
-        db.lock_tables(Build_Process.Data.all_tables)
-        body
-      }
   }
 }
 
@@ -796,7 +786,7 @@
     synchronized {
       _database match {
         case None => body
-        case Some(db) => Build_Process.Data.transaction_lock(db, body)
+        case Some(db) => db.transaction_lock(Build_Process.Data.all_tables)(body)
       }
     }