tuned;
authorwenzelm
Tue Nov 03 16:35:00 2015 +0100 (2015-11-03)
changeset 6155868b86028e02a
parent 61557 f6387515f951
child 61559 313eca3fa847
tuned;
src/Pure/General/exn.scala
src/Tools/jEdit/src/scala_console.scala
     1.1 --- a/src/Pure/General/exn.scala	Tue Nov 03 14:03:44 2015 +0100
     1.2 +++ b/src/Pure/General/exn.scala	Tue Nov 03 16:35:00 2015 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4      def apply(): Throwable = new InterruptedException
     1.5      def unapply(exn: Throwable): Boolean = is_interrupt(exn)
     1.6  
     1.7 -    def expose() { if (Thread.interrupted()) throw apply() }
     1.8 +    def expose() { if (Thread.interrupted) throw apply() }
     1.9      def impose() { Thread.currentThread.interrupt }
    1.10  
    1.11      def postpone[A](body: => A): Option[A] =
    1.12 @@ -104,4 +104,3 @@
    1.13    def message(exn: Throwable): String =
    1.14      user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
    1.15  }
    1.16 -
     2.1 --- a/src/Tools/jEdit/src/scala_console.scala	Tue Nov 03 14:03:44 2015 +0100
     2.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Tue Nov 03 16:35:00 2015 +0100
     2.3 @@ -165,7 +165,7 @@
     2.4            }
     2.5            finally {
     2.6              running.change(_ => None)
     2.7 -            Thread.interrupted()
     2.8 +            Thread.interrupted
     2.9            }
    2.10            GUI_Thread.later {
    2.11              if (err != null) err.commandDone()