equal
deleted
inserted
replaced
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 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 |
|