src/Pure/General/exn.scala
changeset 73367 77ef8bef0593
parent 73340 0ffcad1f6130
child 73729 4b1d8beed8a3
equal deleted inserted replaced
73366:5f388e514ab8 73367:77ef8bef0593
   100     }
   100     }
   101 
   101 
   102     def apply(): Throwable = new InterruptedException("Interrupt")
   102     def apply(): Throwable = new InterruptedException("Interrupt")
   103     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
   103     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
   104 
   104 
   105     def dispose(): Unit = Thread.interrupted
   105     def dispose(): Unit = Thread.interrupted()
   106     def expose(): Unit = if (Thread.interrupted) throw apply()
   106     def expose(): Unit = if (Thread.interrupted()) throw apply()
   107     def impose(): Unit = Thread.currentThread.interrupt
   107     def impose(): Unit = Thread.currentThread.interrupt()
   108 
   108 
   109     val return_code = 130
   109     val return_code = 130
   110   }
   110   }
   111 
   111 
   112 
   112