# HG changeset patch
# User wenzelm
# Date 1297182981 -3600
# Node ID 05514b09bb4b03c8c4376f7bc3aad6522a3efcc9
# Parent  8a1ab91df3012fa5df70fa853e70cb2347b62e59
discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;

diff -r 8a1ab91df301 -r 05514b09bb4b NEWS
--- a/NEWS	Tue Feb 08 17:27:18 2011 +0100
+++ b/NEWS	Tue Feb 08 17:36:21 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.
+
 
 *** Document preparation ***
 
diff -r 8a1ab91df301 -r 05514b09bb4b src/Pure/Concurrent/time_limit_dummy.ML
--- a/src/Pure/Concurrent/time_limit_dummy.ML	Tue Feb 08 17:27:18 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 8a1ab91df301 -r 05514b09bb4b src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Feb 08 17:27:18 2011 +0100
+++ b/src/Pure/IsaMakefile	Tue Feb 08 17:36:21 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 8a1ab91df301 -r 05514b09bb4b src/Pure/ML-Systems/polyml-5.2.ML
--- a/src/Pure/ML-Systems/polyml-5.2.ML	Tue Feb 08 17:27:18 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 8a1ab91df301 -r 05514b09bb4b src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Tue Feb 08 17:27:18 2011 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Feb 08 17:36:21 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 8a1ab91df301 -r 05514b09bb4b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Feb 08 17:27:18 2011 +0100
+++ b/src/Pure/ROOT.ML	Tue Feb 08 17:36:21 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 8a1ab91df301 -r 05514b09bb4b src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Feb 08 17:27:18 2011 +0100
+++ b/src/Pure/pure_setup.ML	Tue Feb 08 17:36:21 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"