changeset 56670 | 3f23441453d0 |
parent 56667 | 65e84b0ef974 |
child 56671 | 06853449cf0a |
--- 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 {