diff -r c537905c2125 -r 9d9b30741fc4 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Mon Mar 06 15:12:37 2023 +0100 +++ b/src/Pure/General/sql.scala Mon Mar 06 15:38:50 2023 +0100 @@ -377,7 +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 execute_statement(sql: Source, body: Statement => Unit = _ => ()): Unit = + using_statement(sql) { stmt => body(stmt); stmt.execute() } def update_date(stmt: Statement, i: Int, date: Date): Unit def date(res: Result, column: Column): Date @@ -543,14 +544,14 @@ // see https://www.postgresql.org/docs/current/sql-notify.html def listen(name: String): Unit = - using_statement("LISTEN " + SQL.ident(name))(_.execute()) + execute_statement("LISTEN " + SQL.ident(name)) def unlisten(name: String = "*"): Unit = - using_statement("UNLISTEN " + (if (name == "*") name else SQL.ident(name)))(_.execute()) + execute_statement("UNLISTEN " + (if (name == "*") name else SQL.ident(name))) def notify(name: String, payload: String = ""): Unit = - using_statement( - "NOTIFY " + SQL.ident(name) + if_proper(payload, ", " + SQL.string(payload)))(_.execute()) + execute_statement( + "NOTIFY " + SQL.ident(name) + if_proper(payload, ", " + SQL.string(payload))) def get_notifications(): List[PGNotification] = the_postgresql_connection.getNotifications() match {