src/Pure/ML-Systems/time_limit.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29564 f8b933a62151
permissions -rw-r--r--
use long names for old-style fold combinators;
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