# HG changeset patch
# User wenzelm
# Date 1678821948 -3600
# Node ID f5d3ade80d1580df0e29926c4ce99e8beec9df39
# Parent  c82d49a56cf976064efdf83205d35eb65ab03f98
more specific vacuum operation, which is also relevant to PostgreSQL;

diff -r c82d49a56cf9 -r f5d3ade80d15 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Mar 14 20:06:37 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Tue Mar 14 20:25:48 2023 +0100
@@ -903,7 +903,7 @@
             db2.create_view(Data.universal_table)
           }
         }
-        db2.rebuild()
+        db2.vacuum()
       }
     }
 
diff -r c82d49a56cf9 -r f5d3ade80d15 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Mar 14 20:06:37 2023 +0100
+++ b/src/Pure/General/sql.scala	Tue Mar 14 20:25:48 2023 +0100
@@ -217,6 +217,7 @@
 
   object Tables {
     def list(list: List[Table]): Tables = new Tables(list)
+    val empty: Tables = list(Nil)
     def apply(args: Table*): Tables = list(args.toList)
   }
 
@@ -350,7 +351,7 @@
     def is_sqlite: Boolean = isInstanceOf[SQLite.Database]
     def is_postgresql: Boolean = isInstanceOf[PostgreSQL.Database]
 
-    def rebuild(): Unit = ()
+    def vacuum(tables: SQL.Tables = SQL.Tables.empty): Unit
 
     def now(): Date
 
@@ -483,7 +484,9 @@
 
   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
     override def toString: String = name
-    override def rebuild(): Unit = execute_statement("VACUUM")
+
+    override def vacuum(tables: SQL.Tables = SQL.Tables.empty): Unit =
+      execute_statement("VACUUM")  // always FULL
 
     override def now(): Date = Date.now()
 
@@ -565,6 +568,9 @@
   ) extends SQL.Database {
     override def toString: String = name
 
+    override def vacuum(tables: SQL.Tables = SQL.Tables.empty): Unit =
+      execute_statement("VACUUM" + if_proper(tables.list, " " + commas(tables.list.map(_.ident))))
+
     override def now(): Date = {
       val now = SQL.Column.date("now")
       execute_query_statementO[Date]("SELECT NOW() as " + now.ident, res => res.date(now))
diff -r c82d49a56cf9 -r f5d3ade80d15 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 20:06:37 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 20:25:48 2023 +0100
@@ -127,7 +127,7 @@
           Data.all_tables.create_lock(db)
           Data.clean_build(db)
         }
-        db.rebuild()
+        db.vacuum(Data.all_tables)
       }
     }