--- a/src/Pure/ML-Systems/polyml-time-limit.ML Mon Aug 01 19:20:46 2005 +0200
+++ b/src/Pure/ML-Systems/polyml-time-limit.ML Mon Aug 01 19:20:47 2005 +0200
@@ -6,29 +6,32 @@
Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
*)
-structure TimeLimit : sig
- exception TimeOut
- val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end = struct
-
- exception TimeOut
+structure TimeLimit:
+sig
+ exception TimeOut
+ val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end =
+struct
+ exception TimeOut
- fun timeLimit t f x =
- let
- datatype ('a, 'b) union =
- INL of 'a | INR of 'b
- val result = Process.channel ()
- fun workerThread () =
- Process.send (result, SOME (INL (f x) handle exn => INR exn))
- val interrupt = Process.console workerThread
- val old_handle = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE
- (fn _ => ((Process.send (result, NONE)) before (interrupt ()))))
- in
- Posix.Process.alarm t;
- case Process.receive result of
- SOME (INL fx) => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
- | SOME (INR exn) => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); raise exn)
- | NONE => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
- end
+ fun timeLimit t f x =
+ let
+ datatype ('a, 'b) union = INL of 'a | INR of 'b
+ val result = Process.channel ()
+ fun workerThread () =
+ Process.send (result, SOME (INL (f x) handle exn => INR exn))
+ val interrupt = Process.console workerThread
+ val old_handle = Signal.signal (Posix.Signal.alrm,
+ Signal.SIG_HANDLE (fn _ => (Process.send (result, NONE)) before (interrupt ())))
+ in
+ Posix.Process.alarm t;
+ case Process.receive result of
+ SOME (INL fx) =>
+ (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
+ | SOME (INR exn) =>
+ (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle);
+ raise exn)
+ | NONE => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
+ end
end;