src/Pure/General/exn.scala

--- a/src/Pure/General/exn.scala	Sun Apr 05 13:24:12 2020 +0200
+++ b/src/Pure/General/exn.scala	Sun Apr 05 21:05:08 2020 +0200
@@ -96,6 +96,7 @@
     def apply(): Throwable = new InterruptedException
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
+    def dispose() { Thread.interrupted }
     def expose() { if (Thread.interrupted) throw apply() }
     def impose() { Thread.currentThread.interrupt }