# HG changeset patch
# User wenzelm
# Date 1677098155 -3600
# Node ID 885842575e2a662b6fe59a64cee911c9a4e95ae5
# Parent  739a9c34c538b8252d200597b70e5c41b51a3d0f
more uniform operations;

diff -r 739a9c34c538 -r 885842575e2a src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Feb 22 21:35:28 2023 +0100
+++ b/src/Pure/General/sql.scala	Wed Feb 22 21:35:55 2023 +0100
@@ -299,6 +299,8 @@
 
     def is_server: Boolean
 
+    def rebuild(): Unit = ()
+
 
     /* types */
 
@@ -411,6 +413,7 @@
   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
     override def toString: String = name
     override def is_server: Boolean = false
+    override def rebuild(): Unit = using_statement("VACUUM")(_.execute())
 
     def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
 
@@ -423,8 +426,6 @@
 
     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
       table.insert_cmd("INSERT OR IGNORE", sql = sql)
-
-    def rebuild(): Unit = using_statement("VACUUM")(_.execute())
   }
 }