src/Pure/ML-Systems/mlworks.ML

 
 (** Compiler-independent timing functions **)
 
 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 *)
 
 (*Can one redirect 'use' directly to an instream?*)
 fun use_text _ _ txt =