--- 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 }
--- a/src/Pure/System/isabelle_system.scala Sun Apr 05 13:24:12 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala Sun Apr 05 21:05:08 2020 +0200
@@ -287,7 +287,7 @@
proc.getInputStream.close
proc.getErrorStream.close
proc.destroy
- Thread.interrupted
+ Exn.Interrupt.dispose()
}
(output, rc)
}
--- a/src/Tools/jEdit/src/scala_console.scala Sun Apr 05 13:24:12 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Sun Apr 05 21:05:08 2020 +0200
@@ -152,7 +152,7 @@
}
finally {
running.change(_ => None)
- Thread.interrupted
+ Exn.Interrupt.dispose()
}
GUI_Thread.later {
if (err != null) err.commandDone()