src/Pure/System/interrupt.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 51250 ca13a14cc52e
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
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