# HG changeset patch
# User wenzelm
# Date 1446564900 -3600
# Node ID 68b86028e02aade5aeb7385c2d0bc1714defa5eb
# Parent  f6387515f9510b4bed3b33002ce2f740f3538e0c
tuned;

diff -r f6387515f951 -r 68b86028e02a src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Nov 03 14:03:44 2015 +0100
+++ b/src/Pure/General/exn.scala	Tue Nov 03 16:35:00 2015 +0100
@@ -58,7 +58,7 @@
     def apply(): Throwable = new InterruptedException
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
-    def expose() { if (Thread.interrupted()) throw apply() }
+    def expose() { if (Thread.interrupted) throw apply() }
     def impose() { Thread.currentThread.interrupt }
 
     def postpone[A](body: => A): Option[A] =
@@ -104,4 +104,3 @@
   def message(exn: Throwable): String =
     user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
 }
-
diff -r f6387515f951 -r 68b86028e02a src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Tue Nov 03 14:03:44 2015 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala	Tue Nov 03 16:35:00 2015 +0100
@@ -165,7 +165,7 @@
           }
           finally {
             running.change(_ => None)
-            Thread.interrupted()
+            Thread.interrupted
           }
           GUI_Thread.later {
             if (err != null) err.commandDone()