src/Pure/ML-Systems/time_limit.ML
author wenzelm
Thu Oct 01 23:27:05 2009 +0200 (2009-10-01)
changeset 32843 c8f5a7c8353f
parent 29564 f8b933a62151
permissions -rw-r--r--
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm@24688
     1
(*  Title:      Pure/ML-Systems/time_limit.ML
wenzelm@24688
     2
    Author:     Makarius
wenzelm@24688
     3
wenzelm@24688
     4
Dummy implementation of NJ's TimeLimit structure.
wenzelm@24688
     5
*)
wenzelm@24688
     6
wenzelm@24688
     7
signature TIME_LIMIT =
wenzelm@24688
     8
sig
wenzelm@24688
     9
  exception TimeOut
wenzelm@24688
    10
  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
wenzelm@24688
    11
end;
wenzelm@24688
    12
wenzelm@24688
    13
structure TimeLimit: TIME_LIMIT =
wenzelm@24688
    14
struct
wenzelm@24688
    15
wenzelm@24688
    16
exception TimeOut;
wenzelm@24688
    17
fun timeLimit _ f x = f x;
wenzelm@24688
    18
wenzelm@24688
    19
end;
wenzelm@24688
    20