detect nested interrupts;

--- 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
   {