src/Pure/ML-Systems/time_limit.ML
author wenzelm
Mon Sep 24 13:52:50 2007 +0200 (2007-09-24)
changeset 24688 a5754ca5c510
child 29564 f8b933a62151
permissions -rw-r--r--
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
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