# HG changeset patch
# User wenzelm
# Date 1674418971 -3600
# Node ID 2f09dc0e6dda6bfef9fe0bdd569b5d5c89a00ec0
# Parent  7b5b1789a34c23812c2b68ec748a1ca8a8a3f9cf
support IPC via database server;

diff -r 7b5b1789a34c -r 2f09dc0e6dda src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jan 22 21:07:25 2023 +0100
+++ b/src/Pure/General/sql.scala	Sun Jan 22 21:22:51 2023 +0100
@@ -11,7 +11,7 @@
 import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
 
 import org.sqlite.jdbc4.JDBC4Connection
-import org.postgresql.PGConnection
+import org.postgresql.{PGConnection, PGNotification}
 
 import scala.collection.mutable
 
@@ -499,6 +499,28 @@
       table.insert_cmd("INSERT",
         sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
 
+
+    /* notifications: IPC via database server */
+    // see https://www.postgresql.org/docs/current/sql-notify.html
+
+    def listen(name: String): Unit =
+      using_statement("LISTEN " + SQL.ident(name))(_.execute())
+
+    def unlisten(name: String = "*"): Unit =
+      using_statement("UNLISTEN " + (if (name == "*") name else SQL.ident(name)))(_.execute())
+
+    def notify(name: String, payload: String = ""): Unit =
+      using_statement(
+        "NOTIFY " + SQL.ident(name) +
+          (if (payload.isEmpty) "" else ", " + SQL.string(payload)))(_.execute())
+
+    def get_notifications(): List[PGNotification] =
+      the_postgresql_connection.getNotifications() match {
+        case null => Nil
+        case array => array.toList
+      }
+
+
     override def close(): Unit = { super.close(); port_forwarding.foreach(_.close()) }
   }
 }