src/Pure/General/exn.scala
changeset 71700 6c39c3be85df
parent 71601 97ccf48c2f0c
child 71705 7b75d52a1bf1
equal deleted inserted replaced
71694:16aa085f9353 71700:6c39c3be85df
    94   object Interrupt
    94   object Interrupt
    95   {
    95   {
    96     def apply(): Throwable = new InterruptedException
    96     def apply(): Throwable = new InterruptedException
    97     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
    97     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
    98 
    98 
       
    99     def dispose() { Thread.interrupted }
    99     def expose() { if (Thread.interrupted) throw apply() }
   100     def expose() { if (Thread.interrupted) throw apply() }
   100     def impose() { Thread.currentThread.interrupt }
   101     def impose() { Thread.currentThread.interrupt }
   101 
   102 
   102     def postpone[A](body: => A): Option[A] =
   103     def postpone[A](body: => A): Option[A] =
   103     {
   104     {