src/Pure/ML-Systems/time_limit.ML
author wenzelm
Mon, 24 Sep 2007 13:52:50 +0200
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);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/time_limit.ML
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     4
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     5
Dummy implementation of NJ's TimeLimit structure.
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     6
*)
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     7
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     8
signature TIME_LIMIT =
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
     9
sig
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    10
  exception TimeOut
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    11
  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    12
end;
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    13
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    14
structure TimeLimit: TIME_LIMIT =
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    15
struct
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    16
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    17
exception TimeOut;
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    18
fun timeLimit _ f x = f x;
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    19
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    20
end;
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents:
diff changeset
    21