--- 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()
--- a/src/Pure/Thy/sessions.scala Mon Mar 06 15:01:44 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Mar 06 15:12:37 2023 +0100
@@ -1552,23 +1552,21 @@
def init_session_info(db: SQL.Database, name: String): Unit = {
db.transaction {
db.create_table(Session_Info.table)
- db.using_statement(
- Session_Info.table.delete(sql = Session_Info.session_name.where_equal(name)))(_.execute())
- if (db.isInstanceOf[PostgreSQL.Database]) {
- db.using_statement(Session_Info.augment_table)(_.execute())
- }
+ db.execute_statement(
+ Session_Info.table.delete(sql = Session_Info.session_name.where_equal(name)))
+ if (db.isInstanceOf[PostgreSQL.Database]) db.execute_statement(Session_Info.augment_table)
db.create_table(Sources.table)
- db.using_statement(Sources.table.delete(sql = Sources.where_equal(name)))(_.execute())
+ db.execute_statement(Sources.table.delete(sql = Sources.where_equal(name)))
db.create_table(Export.Data.table)
- db.using_statement(
- Export.Data.table.delete(sql = Export.Data.session_name.where_equal(name)))(_.execute())
+ db.execute_statement(
+ Export.Data.table.delete(sql = Export.Data.session_name.where_equal(name)))
db.create_table(Document_Build.Data.table)
- db.using_statement(
+ db.execute_statement(
Document_Build.Data.table.delete(
- sql = Document_Build.Data.session_name.where_equal(name)))(_.execute())
+ sql = Document_Build.Data.session_name.where_equal(name)))
}
}
--- a/src/Pure/Tools/build_process.scala Mon Mar 06 15:01:44 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Mar 06 15:12:37 2023 +0100
@@ -313,7 +313,7 @@
if (old.nonEmpty) {
for (table <- List(Base.table, Sessions.table, Progress.table, Workers.table)) {
- db.using_statement(table.delete(sql = Generic.build_uuid.where_member(old)))(_.execute())
+ db.execute_statement(table.delete(sql = Generic.build_uuid.where_member(old)))
}
}
}
@@ -447,9 +447,8 @@
def set_serial(db: SQL.Database, worker_uuid: String, build_uuid: String, serial: Long): Unit = {
if (get_serial(db, worker_uuid = worker_uuid) != serial) {
- db.using_statement(
- Workers.table.delete(sql = SQL.where(Generic.sql(worker_uuid = worker_uuid)))
- )(_.execute())
+ db.execute_statement(
+ Workers.table.delete(sql = SQL.where(Generic.sql(worker_uuid = worker_uuid))))
db.using_statement(Workers.table.insert()) { stmt =>
stmt.string(1) = worker_uuid
stmt.string(2) = build_uuid
@@ -487,9 +486,8 @@
val (delete, insert) = Library.symmetric_difference(old_pending, pending)
if (delete.nonEmpty) {
- db.using_statement(
- Pending.table.delete(
- sql = SQL.where(Generic.sql(names = delete.map(_.name)))))(_.execute())
+ db.execute_statement(
+ Pending.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.name)))))
}
for (entry <- insert) {
@@ -533,9 +531,8 @@
val (delete, insert) = Library.symmetric_difference(old_running, abs_running)
if (delete.nonEmpty) {
- db.using_statement(
- Running.table.delete(
- sql = SQL.where(Generic.sql(names = delete.map(_.job_name)))))(_.execute())
+ db.execute_statement(
+ Running.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.job_name)))))
}
for (job <- insert) {
--- a/src/Pure/Tools/server.scala Mon Mar 06 15:01:44 2023 +0100
+++ b/src/Pure/Tools/server.scala Mon Mar 06 15:12:37 2023 +0100
@@ -398,8 +398,7 @@
Isabelle_System.chmod("600", Data.database)
db.create_table(Data.table)
list(db).filterNot(_.active).foreach(server_info =>
- db.using_statement(
- Data.table.delete(sql = Data.name.where_equal(server_info.name)))(_.execute()))
+ db.execute_statement(Data.table.delete(sql = Data.name.where_equal(server_info.name))))
}
db.transaction {
find(db, name) match {
@@ -410,7 +409,7 @@
val server = new Server(port, log)
val server_info = Info(name, server.port, server.password)
- db.using_statement(Data.table.delete(sql = Data.name.where_equal(name)))(_.execute())
+ db.execute_statement(Data.table.delete(sql = Data.name.where_equal(name)))
db.using_statement(Data.table.insert()) { stmt =>
stmt.string(1) = server_info.name
stmt.int(2) = server_info.port