1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/polyml-time-limit.ML	Tue Jun 01 00:17:07 2004 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +(*  Title:      Pure/ML-Systems/polyml-time-limit.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tjark Weber
     1.7 +    Copyright   2004
     1.8 +
     1.9 +Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
    1.10 +*)
    1.11 +
    1.12 +structure TimeLimit : sig
    1.13 +	exception TimeOut
    1.14 +	val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
    1.15 +end = struct
    1.16 +
    1.17 +	exception TimeOut
    1.18 +
    1.19 +	fun timeLimit t f x =
    1.20 +	let
    1.21 +		datatype ('a, 'b) union =
    1.22 +			INL of 'a | INR of 'b
    1.23 +		val result = Process.channel ()
    1.24 +		fun workerThread () =
    1.25 +			Process.send (result, SOME (INL (f x) handle exn => INR exn))
    1.26 +		val interrupt = Process.console workerThread
    1.27 +		val old_handle = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE
    1.28 +			(fn _ => ((Process.send (result, NONE)) before (interrupt ()))))
    1.29 +	in
    1.30 +		Posix.Process.alarm t;
    1.31 +		case Process.receive result of
    1.32 +		  SOME (INL fx)  => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
    1.33 +		| SOME (INR exn) => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); raise exn)
    1.34 +		| NONE           => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
    1.35 +	end
    1.36 +
    1.37 +end;