# HG changeset patch
# User webertj
# Date 1138033792 -3600
# Node ID 97aaecb84afe73dabd984f62ef0576adc38b9b71
# Parent  2f55e3e473557138ec7f9becf38299cb1cfb35d5
TimeLimit replaced by interrupt_timeout

diff -r 2f55e3e47355 -r 97aaecb84afe src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Mon Jan 23 15:23:31 2006 +0100
+++ b/src/HOL/Tools/refute.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -923,8 +923,6 @@
 (* {...}     : parameters that control the translation/model generation      *)
 (* t         : term to be translated into a propositional formula            *)
 (* negate    : if true, find a model that makes 't' false (rather than true) *)
-(* Note: exception 'TimeOut' is raised if the algorithm does not terminate   *)
-(*       within 'maxtime' seconds (if 'maxtime' >0)                          *)
 (* ------------------------------------------------------------------------- *)
 
 	(* theory -> params -> Term.term -> bool -> unit *)
@@ -1014,9 +1012,9 @@
 			writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": "
 				^ Sign.string_of_term (sign_of thy) t);
 			if maxtime>0 then (
-				TimeLimit.timeLimit (Time.fromSeconds (Int.toLarge maxtime))
+				interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime))
 					wrapper ()
-				handle TimeLimit.TimeOut =>
+				handle Interrupt =>
 					writeln ("\nSearch terminated, time limit ("
 						^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds")
 						^ ") exceeded.")
diff -r 2f55e3e47355 -r 97aaecb84afe src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Jan 23 15:23:31 2006 +0100
+++ b/src/Pure/IsaMakefile	Mon Jan 23 17:29:52 2006 +0100
@@ -45,9 +45,10 @@
   Isar/session.ML Isar/skip_proof.ML Isar/specification.ML Isar/term_style.ML	\
   Isar/thy_header.ML Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML             \
   ML-Systems/cpu-timer-gc.ML ML-Systems/polyml-posix.ML                         \
-  ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML                          \
+  ML-Systems/polyml-interrupt-timeout.ML ML-Systems/polyml.ML                   \
   ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML                   \
   ML-Systems/poplogml.ML ML-Systems/smlnj-basis-compat.ML                       \
+  ML-Systems/smlnj-interrupt-timeout.ML                                         \
   ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-pp-new.ML                       \
   ML-Systems/smlnj-pp-old.ML ML-Systems/smlnj-ptreql.ML                         \
   ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML          \
diff -r 2f55e3e47355 -r 97aaecb84afe src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Mon Jan 23 15:23:31 2006 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -98,16 +98,8 @@
 (* bounded time execution *)
 
 (* FIXME proper implementation available? *)
-
-structure TimeLimit : sig
-   exception TimeOut
-   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end = struct
-   exception TimeOut
-   fun timeLimit t f x =
-      f x;
-end;
-
+fun interrupt_timeout time f x =
+  f x;
 
 (* ML command execution *)
 
diff -r 2f55e3e47355 -r 97aaecb84afe src/Pure/ML-Systems/polyml-interrupt-timeout.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-interrupt-timeout.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -0,0 +1,44 @@
+(*  Title:      Pure/ML-Systems/polyml-interrupt-timeout.ML
+    ID:         $Id$
+    Author:     Tjark Weber, Makarius
+    Copyright   2006
+
+Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
+*)
+
+local
+
+  val alarm_active = ref false;
+
+  val _ = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE (fn _ =>
+    let val active = ! alarm_active in
+      alarm_active := false;
+      if active then
+        Process.interruptConsoleProcesses ()
+      else
+        ()
+    end));
+
+in
+
+  (* Time.time -> ('a -> 'b) -> 'a -> 'b *)
+
+  fun interrupt_timeout time f x =
+  let
+    fun deactivate_alarm () = (
+      alarm_active := false;
+      Posix.Process.alarm Time.zeroTime
+    )
+  in
+    alarm_active := true;
+    Posix.Process.alarm time;
+    let val result = f x in
+      deactivate_alarm ();
+      result
+    end handle exn => (
+      deactivate_alarm ();
+      raise exn
+    )
+  end;
+
+end;
diff -r 2f55e3e47355 -r 97aaecb84afe src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Jan 23 15:23:31 2006 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -62,8 +62,12 @@
 
 (* bounded time execution *)
 
+(* FIXME proper implementation for Cygwin available? *)
+fun interrupt_timeout time f x =
+  f x;
+
 unless_cygwin
-  use "ML-Systems/polyml-time-limit.ML";
+  use "ML-Systems/polyml-interrupt-timeout.ML";
 
 
 (* prompts *)
diff -r 2f55e3e47355 -r 97aaecb84afe src/Pure/ML-Systems/poplogml.ML
--- a/src/Pure/ML-Systems/poplogml.ML	Mon Jan 23 15:23:31 2006 +0100
+++ b/src/Pure/ML-Systems/poplogml.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -269,6 +269,12 @@
 end;
 
 
+(* bounded time execution *)
+
+(* FIXME proper implementation available? *)
+fun interrupt_timeout time f x =
+  f x;
+
 
 (** interrupts **)      (*Note: may get into race conditions*)
 
diff -r 2f55e3e47355 -r 97aaecb84afe src/Pure/ML-Systems/smlnj-interrupt-timeout.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/smlnj-interrupt-timeout.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -0,0 +1,11 @@
+(*  Title:      Pure/ML-Systems/smlnj-interrupt-timeout.ML
+    ID:         $Id$
+    Author:     Tjark Weber, Makarius
+    Copyright   2006
+
+Bounded time execution (similar to SML/NJ's TimeLimit structure).
+*)
+
+fun interrupt_timeout time f x =
+  TimeLimit.timeLimit time f x
+    handle TimeLimit.TimeOut => raise SML90.Interrupt;
diff -r 2f55e3e47355 -r 97aaecb84afe src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Jan 23 15:23:31 2006 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -59,6 +59,11 @@
 | _ => use "ML-Systems/cpu-timer-gc.ML");
 
 
+(* bounded time execution *)
+
+use "ML-Systems/smlnj-interrupt-timeout.ML";
+
+
 (*prompts*)
 fun ml_prompts p1 p2 =
   (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);