# HG changeset patch
# User wenzelm
# Date 1586113508 -7200
# Node ID 6c39c3be85df7b1c4040fee34411fce07e21eaa7
# Parent  16aa085f935330f4f93403f94b7caef929fead7e
clarified signature;

diff -r 16aa085f9353 -r 6c39c3be85df 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 }
 
diff -r 16aa085f9353 -r 6c39c3be85df src/Pure/System/isabelle_system.scala
--- 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)
   }
diff -r 16aa085f9353 -r 6c39c3be85df src/Tools/jEdit/src/scala_console.scala
--- 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()