# HG changeset patch
# User webertj
# Date 1086041827 -7200
# Node ID 73a0a6e0426ab78c914d5eea5a7f272e87f203df
# Parent  83f1dc18f1f1524a2eb3260cd2fed816dc1edd42
SML/NJs TimeLimit structure ported to Poly/ML

diff -r 83f1dc18f1f1 -r 73a0a6e0426a src/Pure/ML-Systems/polyml-time-limit.ML
--- /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;