# HG changeset patch
# User wenzelm
# Date 1398251111 -7200
# Node ID 3f23441453d0b2232bcac7e6d20671918f71db95
# Parent  f42717b5dc84301a339a71ea0d36b67605cc9466
detect nested interrupts;

diff -r f42717b5dc84 -r 3f23441453d0 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Wed Apr 23 12:55:57 2014 +0200
+++ b/src/Pure/General/exn.scala	Wed Apr 23 13:05:11 2014 +0200
@@ -30,7 +30,15 @@
   /* interrupts */
 
   def is_interrupt(exn: Throwable): Boolean =
-    exn.isInstanceOf[InterruptedException]
+  {
+    var found_interrupt = false
+    var e = exn
+    while (!found_interrupt && e != null) {
+      found_interrupt |= e.isInstanceOf[InterruptedException]
+      e = e.getCause
+    }
+    found_interrupt
+  }
 
   object Interrupt
   {