--- 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.")
--- 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 \
--- 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 *)
--- /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;
--- 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 *)
--- 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*)
--- /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;
--- 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);