# HG changeset patch
# User wenzelm
# Date 1190634770 -7200
# Node ID a5754ca5c5107c42577639026bb580c79ccce638
# Parent  f24306b9e0731f33f4d96a05ab62ffb70a4edf8b
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);

diff -r f24306b9e073 -r a5754ca5c510 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sun Sep 23 23:39:42 2007 +0200
+++ b/src/HOL/Tools/refute.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -1240,9 +1240,9 @@
         ^ (if negate then "refutes" else "satisfies") ^ ": "
         ^ Sign.string_of_term thy t);
       if maxtime>0 then (
-        interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime))
+        TimeLimit.timeLimit (Time.fromSeconds maxtime)
           wrapper ()
-        handle Interrupt =>
+        handle TimeLimit.TimeOut =>
           writeln ("\nSearch terminated, time limit (" ^ string_of_int maxtime
             ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")
       ) else
diff -r f24306b9e073 -r a5754ca5c510 src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Sun Sep 23 23:39:42 2007 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -16,7 +16,8 @@
 val ml_system_fix_ints = false;
 
 use "ML-Systems/exn.ML";
-use "ML-Systems/multithreading_dummy.ML";
+use "ML-Systems/multithreading.ML";
+use "ML-Systems/time_limit.ML";
 
 
 fun exit 0 = (OS.Process.exit OS.Process.success): unit
@@ -125,13 +126,6 @@
 end;
 
 
-(* bounded time execution *)
-
-(*dummy implementation*)
-fun interrupt_timeout time f x =
-  f x;
-
-
 
 (** OS related **)
 
diff -r f24306b9e073 -r a5754ca5c510 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sun Sep 23 23:39:42 2007 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -32,7 +32,8 @@
 load "IO";
 
 use "ML-Systems/exn.ML";
-use "ML-Systems/multithreading_dummy.ML";
+use "ML-Systems/multithreading.ML";
+use "ML-Systems/time_limit.ML";
 
 
 (*low-level pointer equality*)
@@ -141,13 +142,6 @@
 end;
 
 
-(* bounded time execution *)
-
-(*dummy implementation*)
-fun interrupt_timeout time f x =
-  f x;
-
-
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
diff -r f24306b9e073 -r a5754ca5c510 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Sep 23 23:39:42 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -12,7 +12,7 @@
   include MULTITHREADING
   val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
   val raise_interrupt: ('a -> 'b) -> 'a -> 'b
-  val interrupt_timeout: Time.time -> ('a -> 'b) -> 'a -> 'b
+  structure TimeLimit: TIME_LIMIT
 end;
 
 structure Multithreading: MULTITHREADING =
@@ -72,15 +72,30 @@
 fun ignore_interrupt f = uninterruptible (fn _ => f);
 fun raise_interrupt f = interruptible (fn _ => f);
 
-fun interrupt_timeout time f x =
+
+(* execution with time limit *)
+
+structure TimeLimit =
+struct
+
+exception TimeOut;
+
+fun timeLimit time f x =
   uninterruptible (fn atts => fn () =>
     let
       val worker = Thread.self ();
+      val timeout = ref false;
       val watchdog = Thread.fork (interruptible (fn _ => fn () =>
-        (OS.Process.sleep time; Thread.interrupt worker)), []);
+        (OS.Process.sleep time; timeout := true; Thread.interrupt worker)), []);
+
+      (*RACE! timeout signal vs. external Interrupt*)
       val result = Exn.capture (with_attributes atts (fn _ => f)) x;
+      val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false);
+
       val _ = Thread.interrupt watchdog handle Thread _ => ();
-    in Exn.release result end) ();
+    in if was_timeout then raise TimeOut else Exn.release result end) ();
+
+end;
 
 
 (* critical section -- may be nested within the same thread *)
@@ -216,7 +231,9 @@
 
 val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
 val CRITICAL = Multithreading.CRITICAL;
+
 val ignore_interrupt = Multithreading.ignore_interrupt;
 val raise_interrupt = Multithreading.raise_interrupt;
-val interrupt_timeout = Multithreading.interrupt_timeout;
 
+structure TimeLimit = Multithreading.TimeLimit;
+
diff -r f24306b9e073 -r a5754ca5c510 src/Pure/ML-Systems/polyml-interrupt-timeout.ML
--- a/src/Pure/ML-Systems/polyml-interrupt-timeout.ML	Sun Sep 23 23:39:42 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/ML-Systems/polyml-interrupt-timeout.ML
-    ID:         $Id$
-    Author:     Tjark Weber
-    Copyright   2006-2007
-
-Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
-*)
-
-(* Note: This code may cause an infrequent segmentation fault (due to a race
-         condition between process creation/termination and garbage collection)
-         before PolyML 5.0. *)
-
-(* Note: The timer process sometimes does not receive enough CPU time to put
-         itself to sleep.  It then cannot indicate a timeout when (or soon
-         after) the specified time has elapsed.  This issue is obviously caused
-         by the process scheduling algorithm in current PolyML versions.  We
-         could use additional communication between the timer and the worker
-         process to ensure that the timer receives /some/ CPU time, but there
-         seems to be no way to guarantee that the timer process receives
-         sufficient CPU time to complete its task. *)
-
-(* Note: f must not manipulate the timer used by Posix.Process.sleep *)
-
-fun interrupt_timeout time f x =
-let
-  val ch = Process.channel ()
-  val interrupt_timer = Process.console (fn () =>
-    (Posix.Process.sleep time; Process.send (ch, NONE)))
-  val interrupt_worker = Process.console (fn () =>
-    Process.send (ch, SOME (Exn.capture f x)))
-in
-  case Process.receive ch of
-    NONE    => (interrupt_worker (); raise Interrupt)
-  | SOME fx => (interrupt_timer (); Exn.release fx)
-end;
diff -r f24306b9e073 -r a5754ca5c510 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sun Sep 23 23:39:42 2007 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -5,7 +5,8 @@
 *)
 
 use "ML-Systems/exn.ML";
-use "ML-Systems/multithreading_dummy.ML";
+use "ML-Systems/multithreading.ML";
+use "ML-Systems/time_limit.ML";
 
 val ml_system_fix_ints = false;
 
@@ -60,13 +61,6 @@
   in (sys, usr, gc) end;
 
 
-(* bounded time execution *)
-
-(*dummy implementation*)
-fun interrupt_timeout time f x =
-  f x;
-
-
 (* prompts *)
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
diff -r f24306b9e073 -r a5754ca5c510 src/Pure/ML-Systems/poplogml.ML
--- a/src/Pure/ML-Systems/poplogml.ML	Sun Sep 23 23:39:42 2007 +0200
+++ b/src/Pure/ML-Systems/poplogml.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -272,12 +272,6 @@
 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 f24306b9e073 -r a5754ca5c510 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sun Sep 23 23:39:42 2007 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -7,7 +7,7 @@
 use "ML-Systems/proper_int.ML";
 use "ML-Systems/overloading_smlnj.ML";
 use "ML-Systems/exn.ML";
-use "ML-Systems/multithreading_dummy.ML";
+use "ML-Systems/multithreading.ML";
 
 
 (*low-level pointer equality*)
@@ -169,13 +169,6 @@
 end;
 
 
-(* bounded time execution *)
-
-fun interrupt_timeout time f x =
-  TimeLimit.timeLimit time f x
-    handle TimeLimit.TimeOut => raise Interrupt;
-
-
 (** Signal handling: emulation of the Poly/ML Signal structure. Note that types
     Posix.Signal.signal and Signals.signal differ **)
 
diff -r f24306b9e073 -r a5754ca5c510 src/Pure/ML-Systems/time_limit.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/time_limit.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -0,0 +1,21 @@
+(*  Title:      Pure/ML-Systems/time_limit.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Dummy implementation of NJ's TimeLimit structure.
+*)
+
+signature TIME_LIMIT =
+sig
+  exception TimeOut
+  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end;
+
+structure TimeLimit: TIME_LIMIT =
+struct
+
+exception TimeOut;
+fun timeLimit _ f x = f x;
+
+end;
+
diff -r f24306b9e073 -r a5754ca5c510 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Sep 23 23:39:42 2007 +0200
+++ b/src/Pure/codegen.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -996,14 +996,14 @@
   in
     if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
     then
-      (case try (fn state => interrupt_timeout (!auto_quickcheck_time_limit)
+      (case try (fn state => TimeLimit.timeLimit (!auto_quickcheck_time_limit)
            (test_goal true (params, []) 1 assms) state) state of
          SOME (cex as SOME _) =>
            Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
              Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
        | _ => state)
     else state
-  end handle Interrupt => state;
+  end handle TimeLimit.TimeOut => state;
 
 val _ = Context.add_setup
   (Context.theory_map (Specification.add_theorem_hook test_goal'));