src/Pure/General/sql.scala
changeset 77541 9d9b30741fc4
parent 77540 c537905c2125
child 77542 2da5562114c5
--- 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 {