# HG changeset patch
# User wenzelm
# Date 1689675552 -7200
# Node ID 41e8ae87184dd74547b595ca0af243d9279dbc21
# Parent  475600ef98b8b4df831a39607288d06ab4c07bf2
clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);

diff -r 475600ef98b8 -r 41e8ae87184d src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Jul 18 11:39:43 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Jul 18 12:19:12 2023 +0200
@@ -631,6 +631,9 @@
   /* SQL data model */
 
   object Data extends SQL.Data("isabelle_build_log") {
+    override def tables: SQL.Tables = ???
+
+
     /* main content */
 
     val log_name = SQL.Column.string("log_name").make_primary_key
diff -r 475600ef98b8 -r 41e8ae87184d src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Jul 18 11:39:43 2023 +0200
+++ b/src/Pure/General/sql.scala	Tue Jul 18 12:19:12 2023 +0200
@@ -230,15 +230,12 @@
 
   object Tables {
     def list(list: List[Table]): Tables = new Tables(list)
-    val empty: Tables = list(Nil)
     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 ::: (other: Tables): Tables = new Tables(other.list ::: list)
-
     def iterator: Iterator[Table] = list.iterator
 
     // requires transaction
@@ -251,7 +248,7 @@
   }
 
   abstract class Data(table_prefix: String = "") {
-    def tables: Tables = Tables.empty
+    def tables: Tables
 
     def transaction_lock[A](
       db: Database,
@@ -384,13 +381,13 @@
     def is_sqlite: Boolean = isInstanceOf[SQLite.Database]
     def is_postgresql: Boolean = isInstanceOf[PostgreSQL.Database]
 
-    def vacuum(tables: SQL.Tables = SQL.Tables.empty): Unit =
-      if (tables.list.nonEmpty) {
+    def vacuum(tables: List[SQL.Table] = Nil): Unit =
+      if (tables.nonEmpty) {
         postgresql_major_version match {
           case Some(m) if m <= 10 =>
             for (table <- tables) execute_statement("VACUUM " + table.ident)
           case Some(_) =>
-            execute_statement("VACUUM" + commas(tables.list.map(_.ident)))
+            execute_statement("VACUUM" + commas(tables.map(_.ident)))
           case None => execute_statement("VACUUM")
         }
       }
diff -r 475600ef98b8 -r 41e8ae87184d src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Jul 18 11:39:43 2023 +0200
+++ b/src/Pure/System/progress.scala	Tue Jul 18 12:19:12 2023 +0200
@@ -291,7 +291,7 @@
         stmt.long(10) = 0L
       })
     }
-    if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.tables)
+    if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.tables.list)
   }
 
   def exit(close: Boolean = false): Unit = synchronized {
diff -r 475600ef98b8 -r 41e8ae87184d src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Jul 18 11:39:43 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Tue Jul 18 12:19:12 2023 +0200
@@ -861,15 +861,18 @@
   private val _build_database: Option[SQL.Database] =
     try {
       for (db <- store.maybe_open_build_database(server = server)) yield {
-        val store_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty
+        val store_tables = db.is_postgresql
         Build_Process.Data.transaction_lock(db,
           create = true,
           label = "Build_Process.build_database"
         ) {
           Build_Process.Data.clean_build(db)
-          store_tables.lock(db, create = true)
+          if (store_tables) Store.Data.tables.lock(db, create = true)
         }
-        if (build_context.master) db.vacuum(Build_Process.Data.tables ::: store_tables)
+        if (build_context.master) {
+          db.vacuum(Build_Process.Data.tables.list :::
+            (if (store_tables) Store.Data.tables.list else Nil))
+        }
         db
       }
     }