# HG changeset patch
# User wenzelm
# Date 1708809054 -3600
# Node ID 5938158733bb8374d4eadd48adc0d3a24dfa3e39
# Parent  a5629eade476b8947a1a9769b9c96f323d4d18f7
clarified signature: avoid hardwired values;

diff -r a5629eade476 -r 5938158733bb src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sat Feb 24 22:07:21 2024 +0100
+++ b/src/Pure/General/sql.scala	Sat Feb 24 22:10:54 2024 +0100
@@ -677,7 +677,8 @@
     password: String,
     database: String = "",
     server: SSH.Server = default_server,
-    server_close: Boolean = false
+    server_close: Boolean = false,
+    receiver_delay: Time = Time.seconds(0.5)
   ): Database = {
     init_jdbc
 
@@ -693,7 +694,7 @@
         if_proper(ssh, " via ssh " + quote(ssh.get.toString))
 
     val connection = DriverManager.getConnection(url, user, password)
-    val db = new Database(connection, print, server, server_close)
+    val db = new Database(connection, print, server, server_close, receiver_delay)
 
     try { db.execute_statement("SET standard_conforming_strings = on") }
     catch { case exn: Throwable => db.close(); throw exn }
@@ -749,7 +750,8 @@
     val connection: Connection,
     print: String,
     server: SSH.Server,
-    server_close: Boolean
+    server_close: Boolean,
+    receiver_delay: Time
   ) extends SQL.Database {
     override def toString: String = print
 
@@ -799,7 +801,7 @@
 
         try {
           while (true) {
-            Isabelle_Thread.interruptible { Time.seconds(0.5).sleep() }
+            Isabelle_Thread.interruptible { receiver_delay.sleep() }
             Option(conn.getNotifications()) match {
               case Some(array) if array.nonEmpty =>
                 synchronized {