tuned signature;
authorwenzelm
Mon May 05 09:41:23 2014 +0200 (2014-05-05)
changeset 568615f827142d89a
parent 56860 dc71c3d0e909
child 56862 e6f7ed54d64e
tuned signature;
src/Pure/General/exn.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/General/exn.scala	Mon May 05 09:24:34 2014 +0200
     1.2 +++ b/src/Pure/General/exn.scala	Mon May 05 09:41:23 2014 +0200
     1.3 @@ -45,7 +45,8 @@
     1.4      def apply(): Throwable = new InterruptedException
     1.5      def unapply(exn: Throwable): Boolean = is_interrupt(exn)
     1.6  
     1.7 -    def expose(): Unit = 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      val return_code = 130
    1.12    }
     2.1 --- a/src/Pure/Tools/build.scala	Mon May 05 09:24:34 2014 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Mon May 05 09:41:23 2014 +0200
     2.3 @@ -814,7 +814,7 @@
     2.4      def sleep()
     2.5      {
     2.6        try { Thread.sleep(500) }
     2.7 -      catch { case Exn.Interrupt() => Thread.currentThread.interrupt }
     2.8 +      catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
     2.9      }
    2.10  
    2.11      @tailrec def loop(