diff -r 2b996a0df1ce -r c537905c2125 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Mon Mar 06 15:01:44 2023 +0100 +++ b/src/Pure/General/sql.scala Mon Mar 06 15:12:37 2023 +0100 @@ -377,6 +377,8 @@ def using_statement[A](sql: Source)(f: Statement => A): A = using(statement(sql))(f) + def execute_statement(sql: Source): Unit = using_statement(sql)(_.execute()) + def update_date(stmt: Statement, i: Int, date: Date): Unit def date(res: Result, column: Column): Date @@ -393,16 +395,15 @@ } def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit = - using_statement(table.create(strict, sql_type) + SQL.separate(sql))(_.execute()) + execute_statement(table.create(strict, sql_type) + SQL.separate(sql)) def create_index(table: Table, name: String, columns: List[Column], strict: Boolean = false, unique: Boolean = false): Unit = - using_statement(table.create_index(name, columns, strict, unique))(_.execute()) + execute_statement(table.create_index(name, columns, strict, unique)) def create_view(table: Table, strict: Boolean = false): Unit = { if (strict || !tables.contains(table.name)) { - val sql = "CREATE VIEW " + table + " AS " + { table.query; table.body } - using_statement(sql)(_.execute()) + execute_statement("CREATE VIEW " + table + " AS " + { table.query; table.body }) } } } @@ -438,7 +439,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()) + override def rebuild(): Unit = execute_statement("VACUUM") override def now(): Date = Date.now()