# HG changeset patch
# User wenzelm
# Date 1708869239 -3600
# Node ID 621676d7fb9ac5658e152c17350c22b8f59983e2
# Parent  abb5eedfeecfa3a664181b5901a1248bc141141c
more robust shutdown: interruptible database connection;

diff -r abb5eedfeecf -r 621676d7fb9a src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Feb 25 13:17:39 2024 +0100
+++ b/src/Pure/General/sql.scala	Sun Feb 25 14:53:59 2024 +0100
@@ -805,8 +805,8 @@
 
         try {
           while (true) {
-            Isabelle_Thread.interruptible { receiver_delay.sleep() }
-            Option(conn.getNotifications()) match {
+            Isabelle_Thread.interruptible { receiver_delay.sleep(); Option(conn.getNotifications())}
+            match {
               case Some(array) if array.nonEmpty =>
                 synchronized {
                   var received = _receiver_buffer.getOrElse(Map.empty)