src/Pure/ML-Systems/time_limit.ML
changeset 24688 a5754ca5c510
child 29564 f8b933a62151
equal deleted inserted replaced
24687:f24306b9e073 24688:a5754ca5c510
       
     1 (*  Title:      Pure/ML-Systems/time_limit.ML
       
     2     ID:         $Id$
       
     3     Author:     Makarius
       
     4 
       
     5 Dummy implementation of NJ's TimeLimit structure.
       
     6 *)
       
     7 
       
     8 signature TIME_LIMIT =
       
     9 sig
       
    10   exception TimeOut
       
    11   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
       
    12 end;
       
    13 
       
    14 structure TimeLimit: TIME_LIMIT =
       
    15 struct
       
    16 
       
    17 exception TimeOut;
       
    18 fun timeLimit _ f x = f x;
       
    19 
       
    20 end;
       
    21