src/Pure/System/posix_interrupt.scala
author wenzelm
Sun, 07 Feb 2021 16:31:43 +0100
changeset 73228 0575cfd2ecfc
parent 59720 f893472fff31
child 73340 0ffcad1f6130
permissions -rw-r--r--
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;

/*  Title:      Pure/System/posix_interrupt.scala
    Author:     Makarius

Support for POSIX interrupts (bypassed on Windows).
*/

package isabelle


import sun.misc.{Signal, SignalHandler}


object POSIX_Interrupt
{
  def handler[A](h: => Unit)(e: => A): A =
  {
    val SIGINT = new Signal("INT")
    val new_handler = new SignalHandler { def handle(s: Signal) { h } }
    val old_handler = Signal.handle(SIGINT, new_handler)
    try { e } finally { Signal.handle(SIGINT, old_handler) }
  }

  def exception[A](e: => A): A =
  {
    val thread = Thread.currentThread
    handler { thread.interrupt } { e }
  }
}