# HG changeset patch
# User wenzelm
# Date 1399065956 -7200
# Node ID 5a598f1eecfdd522446c8684276bef02d875e9f7
# Parent  69531d86d77e9f665877e25233db4c7c49ab8ea6
more robust interrupt handling for Scala_Console, which uses JVM Thread.interrupt instead of POSIX SIGINT;

diff -r 69531d86d77e -r 5a598f1eecfd src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri May 02 23:06:05 2014 +0200
+++ b/src/Pure/Tools/build.scala	Fri May 02 23:25:56 2014 +0200
@@ -38,7 +38,11 @@
 
     @volatile private var is_stopped = false
     def interrupt_handler[A](e: => A): A = Interrupt.handler { is_stopped = true } { e }
-    override def stopped: Boolean = is_stopped
+    override def stopped: Boolean =
+    {
+      if (Thread.interrupted) is_stopped = true
+      is_stopped
+    }
   }
 
 
@@ -807,7 +811,11 @@
     // scheduler loop
     case class Result(current: Boolean, heap: String, rc: Int)
 
-    def sleep(): Unit = Thread.sleep(500)
+    def sleep()
+    {
+      try { Thread.sleep(500) }
+      catch { case Exn.Interrupt() => Thread.currentThread.interrupt }
+    }
 
     @tailrec def loop(
       pending: Queue,