# HG changeset patch
# User webertj
# Date 1086042373 -7200
# Node ID 0fc75361e0c7cbdbd948208ee4afe08a4fce0dc2
# Parent  393a7be7316049cb6f1264e561527fbcd26be86a
TimeLimit structure added (no proper implementation yet)

diff -r 393a7be73160 -r 0fc75361e0c7 src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Tue Jun 01 00:18:01 2004 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Tue Jun 01 00:26:13 2004 +0200
@@ -59,6 +59,18 @@
 
 use "ML-Systems/cpu-timer-gc.ML"
 
+(* bounded time execution *)
+
+(* FIXME proper implementation available? *)
+
+structure TimeLimit : sig
+   exception TimeOut
+   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end = struct
+   exception TimeOut
+   fun timeLimit t f x =
+      f x;
+end;
 
 (* ML command execution *)
 
diff -r 393a7be73160 -r 0fc75361e0c7 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Tue Jun 01 00:18:01 2004 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Jun 01 00:26:13 2004 +0200
@@ -60,6 +60,18 @@
 
 use "ML-Systems/cpu-timer-gc.ML";
 
+(* bounded time execution *)
+
+(* FIXME proper implementation available? *)
+
+structure TimeLimit : sig
+   exception TimeOut
+   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end = struct
+   exception TimeOut
+   fun timeLimit t f x =
+      f x;
+end;
 
 (* ML command execution *)