# HG changeset patch
# User wenzelm
# Date 1586194409 -7200
# Node ID b4b973a7df45ced4b8f5e4c941dec6199cd6e233
# Parent  dd9fc8a3036c5f020f31af1de8dc88be21e1c9fa
more uniform and Java-conformant: change of handler is non-blocking and interrupts should not be exposed prematurely (reverting 220d19f3e074);

diff -r dd9fc8a3036c -r b4b973a7df45 src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Mon Apr 06 14:03:58 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Mon Apr 06 19:33:29 2020 +0200
@@ -162,7 +162,6 @@
     finally {
       handler = old_handler
       if (clear_interrupt) interrupt
-      Exn.Interrupt.expose()
     }
   }
 }