src/Pure/ML-Systems/time_limit.ML
author berghofe
Mon Jan 21 14:18:49 2008 +0100 (2008-01-21)
changeset 25939 ddea202704b4
parent 24688 a5754ca5c510
child 29564 f8b933a62151
permissions -rw-r--r--
Removed Logic.auto_rename.
wenzelm@24688
     1
(*  Title:      Pure/ML-Systems/time_limit.ML
wenzelm@24688
     2
    ID:         $Id$
wenzelm@24688
     3
    Author:     Makarius
wenzelm@24688
     4
wenzelm@24688
     5
Dummy implementation of NJ's TimeLimit structure.
wenzelm@24688
     6
*)
wenzelm@24688
     7
wenzelm@24688
     8
signature TIME_LIMIT =
wenzelm@24688
     9
sig
wenzelm@24688
    10
  exception TimeOut
wenzelm@24688
    11
  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
wenzelm@24688
    12
end;
wenzelm@24688
    13
wenzelm@24688
    14
structure TimeLimit: TIME_LIMIT =
wenzelm@24688
    15
struct
wenzelm@24688
    16
wenzelm@24688
    17
exception TimeOut;
wenzelm@24688
    18
fun timeLimit _ f x = f x;
wenzelm@24688
    19
wenzelm@24688
    20
end;
wenzelm@24688
    21