src/Pure/General/exn.scala
changeset 56860 dc71c3d0e909
parent 56782 433cf57550fa
child 56861 5f827142d89a
--- a/src/Pure/General/exn.scala	Sun May 04 21:35:04 2014 +0200
+++ b/src/Pure/General/exn.scala	Mon May 05 09:24:34 2014 +0200
@@ -45,6 +45,8 @@
     def apply(): Throwable = new InterruptedException
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
+    def expose(): Unit = if (Thread.interrupted()) throw apply()
+
     val return_code = 130
   }