author | wenzelm |
Thu, 09 Aug 2007 23:53:50 +0200 | |
changeset 24208 | f4cafbaa05e4 |
parent 21266 | 288a504c24d6 |
child 24651 | 452962f294a3 |
permissions | -rw-r--r-- |
18760 | 1 |
(* Title: Pure/ML-Systems/polyml-interrupt-timeout.ML |
2 |
ID: $Id$ |
|
21266
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
3 |
Author: Tjark Weber |
18760 | 4 |
Copyright 2006 |
5 |
||
6 |
Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML. |
|
7 |
*) |
|
8 |
||
21266
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
9 |
(* Note: This code may cause an infrequent segmentation fault (due to a race |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
10 |
condition between process creation/termination and garbage collection) |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
11 |
before PolyML 5.0. *) |
18760 | 12 |
|
21266
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
13 |
(* Note: f must not manipulate the timer used by Posix.Process.sleep *) |
18814 | 14 |
|
15 |
fun interrupt_timeout time f x = |
|
21266
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
16 |
let |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
17 |
val ch = Process.channel () |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
18 |
val interrupt_timer = Process.console (fn () => |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
19 |
(Posix.Process.sleep time; Process.send (ch, NONE))) |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
20 |
val interrupt_worker = Process.console (fn () => |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
21 |
Process.send (ch, SOME (capture f x))) |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
22 |
in |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
23 |
case Process.receive ch of |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
24 |
NONE => (interrupt_worker (); raise Interrupt) |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
25 |
| SOME fx => (interrupt_timer (); release fx) |
288a504c24d6
new CCS-based implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset
|
26 |
end; |