equal
deleted
inserted
replaced
|
1 (* Title: Pure/ML-Systems/polyml-interrupt-timeout.ML |
|
2 ID: $Id$ |
|
3 Author: Tjark Weber, Makarius |
|
4 Copyright 2006 |
|
5 |
|
6 Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML. |
|
7 *) |
|
8 |
|
9 local |
|
10 |
|
11 val alarm_active = ref false; |
|
12 |
|
13 val _ = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE (fn _ => |
|
14 let val active = ! alarm_active in |
|
15 alarm_active := false; |
|
16 if active then |
|
17 Process.interruptConsoleProcesses () |
|
18 else |
|
19 () |
|
20 end)); |
|
21 |
|
22 in |
|
23 |
|
24 (* Time.time -> ('a -> 'b) -> 'a -> 'b *) |
|
25 |
|
26 fun interrupt_timeout time f x = |
|
27 let |
|
28 fun deactivate_alarm () = ( |
|
29 alarm_active := false; |
|
30 Posix.Process.alarm Time.zeroTime |
|
31 ) |
|
32 in |
|
33 alarm_active := true; |
|
34 Posix.Process.alarm time; |
|
35 let val result = f x in |
|
36 deactivate_alarm (); |
|
37 result |
|
38 end handle exn => ( |
|
39 deactivate_alarm (); |
|
40 raise exn |
|
41 ) |
|
42 end; |
|
43 |
|
44 end; |