clarified operation: empty means "empty" instead of "full";

--- a/src/Pure/General/sql.scala	Sat Jul 08 16:48:15 2023 +0200
+++ b/src/Pure/General/sql.scala	Sat Jul 08 19:14:09 2023 +0200
@@ -526,7 +526,7 @@
     override def toString: String = name
 
     override def vacuum(tables: SQL.Tables = SQL.Tables.empty): Unit =
-      execute_statement("VACUUM")  // always FULL
+      if (tables.list.nonEmpty) execute_statement("VACUUM")  // always FULL
 
     override def now(): Date = Date.now()
 
@@ -609,7 +609,9 @@
     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))))
+      if (tables.list.nonEmpty) {
+        execute_statement("VACUUM" + if_proper(tables.list, " " + commas(tables.list.map(_.ident))))
+      }
 
     override def now(): Date = {
       val now = SQL.Column.date("now")