src/Pure/System/posix_interrupt.scala
author wenzelm
Thu, 10 Sep 2020 21:14:50 +0200
changeset 72250 13976f92a2d0
parent 59720 f893472fff31
child 73340 0ffcad1f6130
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 56860
diff changeset
     1
/*  Title:      Pure/System/posix_interrupt.scala
51250
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
     3
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
     4
Support for POSIX interrupts (bypassed on Windows).
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
     5
*/
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
     6
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
     7
package isabelle
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
     8
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
     9
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    10
import sun.misc.{Signal, SignalHandler}
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    11
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    12
56860
dc71c3d0e909 tuned signature;
wenzelm
parents: 51250
diff changeset
    13
object POSIX_Interrupt
51250
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    14
{
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    15
  def handler[A](h: => Unit)(e: => A): A =
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    16
  {
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    17
    val SIGINT = new Signal("INT")
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    18
    val new_handler = new SignalHandler { def handle(s: Signal) { h } }
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    19
    val old_handler = Signal.handle(SIGINT, new_handler)
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    20
    try { e } finally { Signal.handle(SIGINT, old_handler) }
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    21
  }
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    22
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    23
  def exception[A](e: => A): A =
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    24
  {
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    25
    val thread = Thread.currentThread
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    26
    handler { thread.interrupt } { e }
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    27
  }
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    28
}
ca13a14cc52e support for POSIX interrupts (bypassed on Windows);
wenzelm
parents:
diff changeset
    29