# HG changeset patch
# User wenzelm
# Date 1689676327 -7200
# Node ID a84f8fca08339bb2f4b24a82e5ea6e3e92b9a1c7
# Parent  41e8ae87184dd74547b595ca0af243d9279dbc21
clarified "vacuum" (again, reverting 0bd366fad888);

diff -r 41e8ae87184d -r a84f8fca0833 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Jul 18 12:19:12 2023 +0200
+++ b/src/Pure/General/sql.scala	Tue Jul 18 12:32:07 2023 +0200
@@ -382,15 +382,12 @@
     def is_postgresql: Boolean = isInstanceOf[PostgreSQL.Database]
 
     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.map(_.ident)))
-          case None => execute_statement("VACUUM")
-        }
+      if (is_sqlite) execute_statement("VACUUM")  // always FULL
+      else if (tables.isEmpty) execute_statement("VACUUM FULL")
+      else if (postgresql_major_version.get <= 10) {
+        for (t <- tables) execute_statement("VACUUM " + t.ident)
       }
+      else execute_statement("VACUUM" + commas(tables.map(_.ident)))
 
     def now(): Date