# HG changeset patch
# User wenzelm
# Date 1708883234 -3600
# Node ID 529a6e35aaa91a1912b174a9ded39b8fb5822601
# Parent  621676d7fb9ac5658e152c17350c22b8f59983e2
tuned signature: follow PostgreSQL syntax instead of JDBC API;

diff -r 621676d7fb9a -r 529a6e35aaa9 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Feb 25 14:53:59 2024 +0100
+++ b/src/Pure/General/sql.scala	Sun Feb 25 18:47:14 2024 +0100
@@ -385,7 +385,7 @@
 
   /* notifications: IPC via database server */
 
-  sealed case class Notification(name: String, parameter: String)
+  sealed case class Notification(channel: String, payload: String)
 
 
   /* database */
@@ -590,12 +590,12 @@
 
     /* notifications (PostgreSQL only) */
 
-    def listen(name: String): Unit = ()
-    def unlisten(name: String = "*"): Unit = ()
-    def send(name: String, parameter: String): Unit = ()
-    final def send(name: String): Unit = send(name, "")
+    def listen(channel: String): Unit = ()
+    def unlisten(channel: String = "*"): Unit = ()
+    def send(channel: String, payload: String): Unit = ()
+    final def send(channel: String): Unit = send(channel, "")
     final def send(notification: Notification): Unit =
-      send(notification.name, notification.parameter)
+      send(notification.channel, notification.payload)
     def receive(filter: Notification => Boolean): Option[List[Notification]] = None
   }
 
@@ -842,17 +842,17 @@
       body
     }
 
-    override def listen(name: String): Unit = synchronized_receiver {
-      execute_statement("LISTEN " + SQL.ident(name))
+    override def listen(channel: String): Unit = synchronized_receiver {
+      execute_statement("LISTEN " + SQL.ident(channel))
     }
 
-    override def unlisten(name: String = "*"): Unit = synchronized_receiver {
-      execute_statement("UNLISTEN " + (if (name == "*") name else SQL.ident(name)))
+    override def unlisten(channel: String = "*"): Unit = synchronized_receiver {
+      execute_statement("UNLISTEN " + (if (channel == "*") channel else SQL.ident(channel)))
     }
 
-    override def send(name: String, parameter: String): Unit = synchronized_receiver {
+    override def send(channel: String, payload: String): Unit = synchronized_receiver {
       execute_statement(
-        "NOTIFY " + SQL.ident(name) + if_proper(parameter, ", " + SQL.string(parameter)))
+        "NOTIFY " + SQL.ident(channel) + if_proper(payload, ", " + SQL.string(payload)))
     }
 
     override def receive(