--- 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 *)
--- 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 *)