# HG changeset patch
# User wenzelm
# Date 1297183123 -3600
# Node ID 2837df4d1c7a9434d4109c3e4febe1fa89f04920
# Parent  ab3f6d76fb236da90f6f650364fd508f56289ac8# Parent  05514b09bb4b03c8c4376f7bc3aad6522a3efcc9
merged

diff -r ab3f6d76fb23 -r 2837df4d1c7a Admin/isatest/settings/at-poly
--- a/Admin/isatest/settings/at-poly	Tue Feb 08 16:10:10 2011 +0100
+++ b/Admin/isatest/settings/at-poly	Tue Feb 08 17:38:43 2011 +0100
@@ -1,7 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
-  POLYML_HOME="/home/polyml/polyml-5.2"
-  ML_SYSTEM="polyml-5.2"
+  POLYML_HOME="/home/polyml/polyml-5.3.0"
+  ML_SYSTEM="polyml-5.3.0"
   ML_PLATFORM="x86-linux"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 500"
diff -r ab3f6d76fb23 -r 2837df4d1c7a NEWS
--- a/NEWS	Tue Feb 08 16:10:10 2011 +0100
+++ b/NEWS	Tue Feb 08 17:38:43 2011 +0100
@@ -10,6 +10,9 @@
 Goal.parallel_proofs_threshold (default 100).  See also isabelle
 usedir option -Q.
 
+* Discontinued support for Poly/ML 5.2, which was the last version
+without proper multithreading and TimeLimit implementation.
+
 
 *** HOL ***
 
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -182,7 +182,8 @@
           if ok then
             Exn.capture (fn () =>
               Multithreading.with_attributes Multithreading.private_interrupts
-                (fn _ => Position.setmp_thread_data pos e ())) ()
+                (fn _ =>
+                  Position.setmp_thread_data pos e () before Multithreading.interrupted ())) ()
           else Exn.interrupt_exn;
       in assign_result group result res end;
   in (result, job) end;
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/Concurrent/time_limit.ML
--- a/src/Pure/Concurrent/time_limit.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/Concurrent/time_limit.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -2,6 +2,13 @@
     Author:     Makarius
 
 Execution with time limit.
+
+Notes:
+
+  * There is considerable overhead due to fork of watchdog thread.
+
+  * In rare situations asynchronous interrupts might be mistaken as
+    timeout event, and turned into exception TimeOut accidentally.
 *)
 
 signature TIME_LIMIT =
@@ -15,18 +22,29 @@
 
 exception TimeOut;
 
-fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
-  let
-    val worker = Thread.self ();
-    val timeout = Unsynchronized.ref false;
-    val watchdog = Thread.fork (fn () =>
-      (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
+val wait_time = seconds 0.0001;
+
+fun timeLimit time f x =
+  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+    let
+      val main = Thread.self ();
+      val timeout = Unsynchronized.ref false;
+      val watchdog = Simple_Thread.fork true (fn () =>
+        (OS.Process.sleep time; timeout := true; Thread.interrupt main));
 
-    val result = Exn.capture (restore_attributes f) x;
-    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
+      val result =
+        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
+
+      val _ = Thread.interrupt watchdog handle Thread _ => ();
+      val _ = while Thread.isActive watchdog do OS.Process.sleep wait_time;
 
-    val _ = Thread.interrupt watchdog handle Thread _ => ();
-  in if was_timeout then raise TimeOut else Exn.release result end) ();
+      val test = Exn.capture Multithreading.interrupted ();
+    in
+      if ! timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+      then raise TimeOut
+      else if Exn.is_interrupt_exn test then Exn.interrupt ()
+      else Exn.release result
+    end);
 
 end;
 
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/Concurrent/time_limit_dummy.ML
--- a/src/Pure/Concurrent/time_limit_dummy.ML	Tue Feb 08 16:10:10 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      Pure/Concurrent/time_limit_dummy.ML
-    Author:     Makarius
-
-Execution with time limit -- dummy version.
-*)
-
-structure TimeLimit: TIME_LIMIT =
-struct
-
-exception TimeOut;
-
-fun timeLimit _ f x = (warning "No timeout support on this ML platform"; f x);
-
-end;
-
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/IsaMakefile	Tue Feb 08 17:38:43 2011 +0100
@@ -30,7 +30,6 @@
   ML-Systems/multithreading_polyml.ML			\
   ML-Systems/overloading_smlnj.ML			\
   ML-Systems/polyml-5.2.1.ML				\
-  ML-Systems/polyml-5.2.ML				\
   ML-Systems/polyml.ML					\
   ML-Systems/polyml_common.ML				\
   ML-Systems/pp_dummy.ML				\
@@ -69,7 +68,6 @@
   Concurrent/synchronized_sequential.ML			\
   Concurrent/task_queue.ML				\
   Concurrent/time_limit.ML				\
-  Concurrent/time_limit_dummy.ML			\
   General/alist.ML					\
   General/antiquote.ML					\
   General/balanced_tree.ML				\
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/Isar/runtime.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -106,10 +106,8 @@
       | exn as EXCURSION_FAIL _ => Exn.Exn exn))
   else f x;
 
-fun controlled_execution f =
-  f
-  |> debugging
-  |> Future.interruptible_task;
+fun controlled_execution f x =
+  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
 
 fun toplevel_error output_exn f x = f x
   handle exn =>
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/ML-Systems/compiler_polyml-5.2.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ML-Systems/compiler_polyml-5.2.ML
 
-Runtime compilation for Poly/ML 5.2 and 5.2.1.
+Runtime compilation for Poly/ML 5.2.x.
 *)
 
 local
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/ML-Systems/compiler_polyml-5.3.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ML-Systems/compiler_polyml-5.3.ML
 
-Runtime compilation for Poly/ML 5.3 and 5.4.
+Runtime compilation for Poly/ML 5.3.0 and 5.4.0.
 *)
 
 local
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -21,6 +21,7 @@
   val public_interrupts: Thread.threadAttribute list
   val private_interrupts: Thread.threadAttribute list
   val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
+  val interrupted: unit -> unit  (*exception Interrupt*)
   val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
   val sync_wait: Thread.threadAttribute list option -> Time.time option ->
     ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
@@ -50,6 +51,8 @@
 val private_interrupts = [];
 fun sync_interrupts _ = [];
 
+fun interrupted () = ();
+
 fun with_attributes _ e = e [];
 
 fun sync_wait _ _ _ _ = Exn.Result true;
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -45,6 +45,9 @@
 val no_interrupts =
   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
 
+val test_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
+
 val public_interrupts =
   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
 
@@ -61,6 +64,14 @@
       Thread.InterruptState Thread.InterruptAsynchOnce
     | x => x);
 
+fun interrupted () =
+  let
+    val orig_atts = safe_interrupts (Thread.getAttributes ());
+    val _ = Thread.setAttributes test_interrupts;
+    val test = Exn.capture Thread.testInterrupt ();
+    val _ = Thread.setAttributes orig_atts;
+  in Exn.release test end;
+
 fun with_attributes new_atts e =
   let
     val orig_atts = safe_interrupts (Thread.getAttributes ());
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/ML-Systems/polyml-5.2.ML
--- a/src/Pure/ML-Systems/polyml-5.2.ML	Tue Feb 08 16:10:10 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(*  Title:      Pure/ML-Systems/polyml-5.2.ML
-
-Compatibility wrapper for Poly/ML 5.2.
-*)
-
-open Thread;
-
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
-end;
-
-fun reraise exn = raise exn;
-
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/multithreading.ML";
-use "ML-Systems/unsynchronized.ML";
-
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-use "ML-Systems/compiler_polyml-5.2.ML";
-use "ML-Systems/pp_polyml.ML";
-use "ML-Systems/pp_dummy.ML";
-
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -73,36 +73,6 @@
 
 
 
-(** interrupts **)
-
-local
-
-val sig_int = 2;
-val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
-
-val _ = Signal.signal (sig_int, default_handler);
-val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
-
-fun change_signal new_handler f x =
-  let
-    (*RACE wrt. other signals!*)
-    val old_handler = Signal.signal (sig_int, new_handler);
-    val result = Exn.capture (f old_handler) x;
-    val _ = Signal.signal (sig_int, old_handler);
-  in Exn.release result end;
-
-in
-
-fun interruptible f = change_signal default_handler (fn _ => f);
-
-fun uninterruptible f =
-  change_signal Signal.SIG_IGN
-    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
-
-end;
-
-
-
 (** OS related **)
 
 (* current directory *)
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ROOT.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -72,9 +72,8 @@
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
 
-use "Concurrent/time_limit.ML";
-if Multithreading.available then ()
-else use "Concurrent/time_limit_dummy.ML";
+if String.isPrefix "smlnj" ml_system then ()
+else use "Concurrent/time_limit.ML";
 
 if Multithreading.available
 then use "Concurrent/bash.ML"
@@ -193,8 +192,7 @@
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
 use "ML/ml_compiler.ML";
-if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
-  String.isPrefix "smlnj" ml_system then ()
+if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
 else use "ML/ml_compiler_polyml-5.3.ML";
 use "ML/ml_context.ML";
 
diff -r ab3f6d76fb23 -r 2837df4d1c7a src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/pure_setup.ML	Tue Feb 08 17:38:43 2011 +0100
@@ -36,7 +36,7 @@
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
 
-if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
+if ml_system = "polyml-5.2.1"
 then use "ML/install_pp_polyml.ML"
 else if String.isPrefix "polyml" ml_system
 then use "ML/install_pp_polyml-5.3.ML"