equal
deleted
inserted
replaced
13 object POSIX_Interrupt |
13 object POSIX_Interrupt |
14 { |
14 { |
15 def handler[A](h: => Unit)(e: => A): A = |
15 def handler[A](h: => Unit)(e: => A): A = |
16 { |
16 { |
17 val SIGINT = new Signal("INT") |
17 val SIGINT = new Signal("INT") |
18 val new_handler = new SignalHandler { def handle(s: Signal) { h } } |
18 val new_handler = new SignalHandler { def handle(s: Signal): Unit = h } |
19 val old_handler = Signal.handle(SIGINT, new_handler) |
19 val old_handler = Signal.handle(SIGINT, new_handler) |
20 try { e } finally { Signal.handle(SIGINT, old_handler) } |
20 try { e } finally { Signal.handle(SIGINT, old_handler) } |
21 } |
21 } |
22 |
22 |
23 def exception[A](e: => A): A = |
23 def exception[A](e: => A): A = |