discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;
authorwenzelm
Tue Feb 08 17:36:21 2011 +0100 (2011-02-08)
changeset 4171805514b09bb4b
parent 41717 8a1ab91df301
child 41728 2837df4d1c7a
discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;
NEWS
src/Pure/Concurrent/time_limit_dummy.ML
src/Pure/IsaMakefile
src/Pure/ML-Systems/polyml-5.2.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ROOT.ML
src/Pure/pure_setup.ML
     1.1 --- a/NEWS	Tue Feb 08 17:27:18 2011 +0100
     1.2 +++ b/NEWS	Tue Feb 08 17:36:21 2011 +0100
     1.3 @@ -10,6 +10,9 @@
     1.4  Goal.parallel_proofs_threshold (default 100).  See also isabelle
     1.5  usedir option -Q.
     1.6  
     1.7 +* Discontinued support for Poly/ML 5.2, which was the last version
     1.8 +without proper multithreading and TimeLimit implementation.
     1.9 +
    1.10  
    1.11  *** Document preparation ***
    1.12  
     2.1 --- a/src/Pure/Concurrent/time_limit_dummy.ML	Tue Feb 08 17:27:18 2011 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,15 +0,0 @@
     2.4 -(*  Title:      Pure/Concurrent/time_limit_dummy.ML
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Execution with time limit -- dummy version.
     2.8 -*)
     2.9 -
    2.10 -structure TimeLimit: TIME_LIMIT =
    2.11 -struct
    2.12 -
    2.13 -exception TimeOut;
    2.14 -
    2.15 -fun timeLimit _ f x = (warning "No timeout support on this ML platform"; f x);
    2.16 -
    2.17 -end;
    2.18 -
     3.1 --- a/src/Pure/IsaMakefile	Tue Feb 08 17:27:18 2011 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Tue Feb 08 17:36:21 2011 +0100
     3.3 @@ -30,7 +30,6 @@
     3.4    ML-Systems/multithreading_polyml.ML			\
     3.5    ML-Systems/overloading_smlnj.ML			\
     3.6    ML-Systems/polyml-5.2.1.ML				\
     3.7 -  ML-Systems/polyml-5.2.ML				\
     3.8    ML-Systems/polyml.ML					\
     3.9    ML-Systems/polyml_common.ML				\
    3.10    ML-Systems/pp_dummy.ML				\
    3.11 @@ -69,7 +68,6 @@
    3.12    Concurrent/synchronized_sequential.ML			\
    3.13    Concurrent/task_queue.ML				\
    3.14    Concurrent/time_limit.ML				\
    3.15 -  Concurrent/time_limit_dummy.ML			\
    3.16    General/alist.ML					\
    3.17    General/antiquote.ML					\
    3.18    General/balanced_tree.ML				\
     4.1 --- a/src/Pure/ML-Systems/polyml-5.2.ML	Tue Feb 08 17:27:18 2011 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,32 +0,0 @@
     4.4 -(*  Title:      Pure/ML-Systems/polyml-5.2.ML
     4.5 -
     4.6 -Compatibility wrapper for Poly/ML 5.2.
     4.7 -*)
     4.8 -
     4.9 -open Thread;
    4.10 -
    4.11 -structure ML_Name_Space =
    4.12 -struct
    4.13 -  open PolyML.NameSpace;
    4.14 -  type T = PolyML.NameSpace.nameSpace;
    4.15 -  val global = PolyML.globalNameSpace;
    4.16 -end;
    4.17 -
    4.18 -fun reraise exn = raise exn;
    4.19 -
    4.20 -use "ML-Systems/polyml_common.ML";
    4.21 -use "ML-Systems/thread_dummy.ML";
    4.22 -use "ML-Systems/multithreading.ML";
    4.23 -use "ML-Systems/unsynchronized.ML";
    4.24 -
    4.25 -val _ = PolyML.Compiler.forgetValue "ref";
    4.26 -val _ = PolyML.Compiler.forgetType "ref";
    4.27 -
    4.28 -val pointer_eq = PolyML.pointerEq;
    4.29 -
    4.30 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    4.31 -
    4.32 -use "ML-Systems/compiler_polyml-5.2.ML";
    4.33 -use "ML-Systems/pp_polyml.ML";
    4.34 -use "ML-Systems/pp_dummy.ML";
    4.35 -
     5.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Tue Feb 08 17:27:18 2011 +0100
     5.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Feb 08 17:36:21 2011 +0100
     5.3 @@ -73,36 +73,6 @@
     5.4  
     5.5  
     5.6  
     5.7 -(** interrupts **)
     5.8 -
     5.9 -local
    5.10 -
    5.11 -val sig_int = 2;
    5.12 -val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
    5.13 -
    5.14 -val _ = Signal.signal (sig_int, default_handler);
    5.15 -val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
    5.16 -
    5.17 -fun change_signal new_handler f x =
    5.18 -  let
    5.19 -    (*RACE wrt. other signals!*)
    5.20 -    val old_handler = Signal.signal (sig_int, new_handler);
    5.21 -    val result = Exn.capture (f old_handler) x;
    5.22 -    val _ = Signal.signal (sig_int, old_handler);
    5.23 -  in Exn.release result end;
    5.24 -
    5.25 -in
    5.26 -
    5.27 -fun interruptible f = change_signal default_handler (fn _ => f);
    5.28 -
    5.29 -fun uninterruptible f =
    5.30 -  change_signal Signal.SIG_IGN
    5.31 -    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
    5.32 -
    5.33 -end;
    5.34 -
    5.35 -
    5.36 -
    5.37  (** OS related **)
    5.38  
    5.39  (* current directory *)
     6.1 --- a/src/Pure/ROOT.ML	Tue Feb 08 17:27:18 2011 +0100
     6.2 +++ b/src/Pure/ROOT.ML	Tue Feb 08 17:36:21 2011 +0100
     6.3 @@ -72,9 +72,8 @@
     6.4  if Multithreading.available then ()
     6.5  else use "Concurrent/synchronized_sequential.ML";
     6.6  
     6.7 -use "Concurrent/time_limit.ML";
     6.8 -if Multithreading.available then ()
     6.9 -else use "Concurrent/time_limit_dummy.ML";
    6.10 +if String.isPrefix "smlnj" ml_system then ()
    6.11 +else use "Concurrent/time_limit.ML";
    6.12  
    6.13  if Multithreading.available
    6.14  then use "Concurrent/bash.ML"
    6.15 @@ -193,8 +192,7 @@
    6.16  use "ML/ml_env.ML";
    6.17  use "Isar/runtime.ML";
    6.18  use "ML/ml_compiler.ML";
    6.19 -if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
    6.20 -  String.isPrefix "smlnj" ml_system then ()
    6.21 +if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
    6.22  else use "ML/ml_compiler_polyml-5.3.ML";
    6.23  use "ML/ml_context.ML";
    6.24  
     7.1 --- a/src/Pure/pure_setup.ML	Tue Feb 08 17:27:18 2011 +0100
     7.2 +++ b/src/Pure/pure_setup.ML	Tue Feb 08 17:36:21 2011 +0100
     7.3 @@ -36,7 +36,7 @@
     7.4  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
     7.5  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
     7.6  
     7.7 -if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
     7.8 +if ml_system = "polyml-5.2.1"
     7.9  then use "ML/install_pp_polyml.ML"
    7.10  else if String.isPrefix "polyml" ml_system
    7.11  then use "ML/install_pp_polyml-5.3.ML"