# HG changeset patch # User wenzelm # Date 1678111957 -3600 # Node ID c537905c2125e38a1745e850dfa870ba7e1485de # Parent 2b996a0df1ced33665528a9bb5c2a1f826c3b93c tuned signature; 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() diff -r 2b996a0df1ce -r c537905c2125 src/Pure/Thy/sessions.scala --- 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))) } } diff -r 2b996a0df1ce -r c537905c2125 src/Pure/Tools/build_process.scala --- 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) { diff -r 2b996a0df1ce -r c537905c2125 src/Pure/Tools/server.scala --- 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