src/Pure/System/posix_interrupt.scala
changeset 56860 dc71c3d0e909
parent 51250 ca13a14cc52e
child 59720 f893472fff31
equal deleted inserted replaced
56856:d940ad3959c5 56860:dc71c3d0e909
       
     1 /*  Title:      Pure/System/interrupt.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Support for POSIX interrupts (bypassed on Windows).
       
     5 */
       
     6 
       
     7 package isabelle
       
     8 
       
     9 
       
    10 import sun.misc.{Signal, SignalHandler}
       
    11 
       
    12 
       
    13 object POSIX_Interrupt
       
    14 {
       
    15   def handler[A](h: => Unit)(e: => A): A =
       
    16   {
       
    17     val SIGINT = new Signal("INT")
       
    18     val new_handler = new SignalHandler { def handle(s: Signal) { h } }
       
    19     val old_handler = Signal.handle(SIGINT, new_handler)
       
    20     try { e } finally { Signal.handle(SIGINT, old_handler) }
       
    21   }
       
    22 
       
    23   def exception[A](e: => A): A =
       
    24   {
       
    25     val thread = Thread.currentThread
       
    26     handler { thread.interrupt } { e }
       
    27   }
       
    28 }
       
    29