--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-time-limit.ML Tue Jun 01 00:17:07 2004 +0200
@@ -0,0 +1,34 @@
+(* Title: Pure/ML-Systems/polyml-time-limit.ML
+ ID: $Id$
+ Author: Tjark Weber
+ Copyright 2004
+
+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
+
+ 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;