src/Pure/System/interrupt.scala
author wenzelm
Sat Feb 23 11:27:45 2013 +0100 (2013-02-23 ago)
changeset 51250 ca13a14cc52e
permissions -rw-r--r--
support for POSIX interrupts (bypassed on Windows);
wenzelm@51250
     1
/*  Title:      Pure/System/interrupt.scala
wenzelm@51250
     2
    Author:     Makarius
wenzelm@51250
     3
wenzelm@51250
     4
Support for POSIX interrupts (bypassed on Windows).
wenzelm@51250
     5
*/
wenzelm@51250
     6
wenzelm@51250
     7
package isabelle
wenzelm@51250
     8
wenzelm@51250
     9
wenzelm@51250
    10
import sun.misc.{Signal, SignalHandler}
wenzelm@51250
    11
wenzelm@51250
    12
wenzelm@51250
    13
object Interrupt
wenzelm@51250
    14
{
wenzelm@51250
    15
  def handler[A](h: => Unit)(e: => A): A =
wenzelm@51250
    16
  {
wenzelm@51250
    17
    val SIGINT = new Signal("INT")
wenzelm@51250
    18
    val new_handler = new SignalHandler { def handle(s: Signal) { h } }
wenzelm@51250
    19
    val old_handler = Signal.handle(SIGINT, new_handler)
wenzelm@51250
    20
    try { e } finally { Signal.handle(SIGINT, old_handler) }
wenzelm@51250
    21
  }
wenzelm@51250
    22
wenzelm@51250
    23
  def exception[A](e: => A): A =
wenzelm@51250
    24
  {
wenzelm@51250
    25
    val thread = Thread.currentThread
wenzelm@51250
    26
    handler { thread.interrupt } { e }
wenzelm@51250
    27
  }
wenzelm@51250
    28
}
wenzelm@51250
    29