changeset 56861 | 5f827142d89a |
parent 56860 | dc71c3d0e909 |
child 56862 | e6f7ed54d64e |
--- a/src/Pure/General/exn.scala Mon May 05 09:24:34 2014 +0200 +++ b/src/Pure/General/exn.scala Mon May 05 09:41:23 2014 +0200 @@ -45,7 +45,8 @@ def apply(): Throwable = new InterruptedException def unapply(exn: Throwable): Boolean = is_interrupt(exn) - def expose(): Unit = if (Thread.interrupted()) throw apply() + def expose() { if (Thread.interrupted()) throw apply() } + def impose() { Thread.currentThread.interrupt } val return_code = 130 }