src/Pure/Tools/build.scala
changeset 56837 5a598f1eecfd
parent 56831 e3ccf0809d51
child 56860 dc71c3d0e909
--- 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,