# HG changeset patch
# User webertj
# Date 1138036848 -3600
# Node ID 4a58895f704c5bf894b5424befc6c63566112e2d
# Parent  97aaecb84afe73dabd984f62ef0576adc38b9b71
TimeLimit replaced by interrupt_timeout

diff -r 97aaecb84afe -r 4a58895f704c src/Pure/ML-Systems/polyml-time-limit.ML
--- a/src/Pure/ML-Systems/polyml-time-limit.ML	Mon Jan 23 17:29:52 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(*  Title:      Pure/ML-Systems/polyml-time-limit.ML
-    ID:         $Id$
-    Author:     Tjark Weber
-    Copyright   2004
-
-Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
-*)
-
-structure TimeLimit:
-sig
-  exception TimeOut
-  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end =
-struct
-  exception TimeOut
-
-  fun timeLimit t f x =
-    let
-      datatype ('a, 'b) union = INL of 'a | INR of 'b
-      val result = Process.channel ()
-      fun workerThread () =
-        Process.send (result, SOME (INL (f x) handle exn => INR exn))
-      val interrupt = Process.console workerThread
-      val old_handle = Signal.signal (Posix.Signal.alrm,
-        Signal.SIG_HANDLE (fn _ => (Process.send (result, NONE)) before (interrupt ())))
-    in
-      Posix.Process.alarm t;
-      case Process.receive result of
-        SOME (INL fx) =>
-          (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
-      | SOME (INR exn) =>
-          (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle);
-           raise exn)
-      | NONE => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
-    end
-
-end;