clarified signature;
authorwenzelm
Sun, 05 Apr 2020 21:05:08 +0200
changeset 71700 6c39c3be85df
parent 71694 16aa085f9353
child 71701 ca926ef898eb
clarified signature;
src/Pure/General/exn.scala
src/Pure/System/isabelle_system.scala
src/Tools/jEdit/src/scala_console.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 }
 
--- 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()