TimeLimit structure added (no proper implementation yet)
authorwebertj
Tue Jun 01 00:26:13 2004 +0200 (2004-06-01)
changeset 148510fc75361e0c7
parent 14850 393a7be73160
child 14852 fffab59e0050
TimeLimit structure added (no proper implementation yet)
src/Pure/ML-Systems/mlworks.ML
src/Pure/ML-Systems/mosml.ML
     1.1 --- a/src/Pure/ML-Systems/mlworks.ML	Tue Jun 01 00:18:01 2004 +0200
     1.2 +++ b/src/Pure/ML-Systems/mlworks.ML	Tue Jun 01 00:26:13 2004 +0200
     1.3 @@ -59,6 +59,18 @@
     1.4  
     1.5  use "ML-Systems/cpu-timer-gc.ML"
     1.6  
     1.7 +(* bounded time execution *)
     1.8 +
     1.9 +(* FIXME proper implementation available? *)
    1.10 +
    1.11 +structure TimeLimit : sig
    1.12 +   exception TimeOut
    1.13 +   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
    1.14 +end = struct
    1.15 +   exception TimeOut
    1.16 +   fun timeLimit t f x =
    1.17 +      f x;
    1.18 +end;
    1.19  
    1.20  (* ML command execution *)
    1.21  
     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Tue Jun 01 00:18:01 2004 +0200
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Tue Jun 01 00:26:13 2004 +0200
     2.3 @@ -60,6 +60,18 @@
     2.4  
     2.5  use "ML-Systems/cpu-timer-gc.ML";
     2.6  
     2.7 +(* bounded time execution *)
     2.8 +
     2.9 +(* FIXME proper implementation available? *)
    2.10 +
    2.11 +structure TimeLimit : sig
    2.12 +   exception TimeOut
    2.13 +   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
    2.14 +end = struct
    2.15 +   exception TimeOut
    2.16 +   fun timeLimit t f x =
    2.17 +      f x;
    2.18 +end;
    2.19  
    2.20  (* ML command execution *)
    2.21