multithreading for Poly/ML 5.1 is no longer supported;
authorwenzelm
Tue Sep 16 18:01:24 2008 +0200 (2008-09-16 ago)
changeset 28254d67ba23e0277
parent 28253 04fc1ba19f93
child 28255 6faea8ad8559
multithreading for Poly/ML 5.1 is no longer supported;
NEWS
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml-5.1.ML
     1.1 --- a/NEWS	Tue Sep 16 17:28:37 2008 +0200
     1.2 +++ b/NEWS	Tue Sep 16 18:01:24 2008 +0200
     1.3 @@ -255,6 +255,9 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 +* Multithreading for Poly/ML 5.1 is no longer supported, only for
     1.8 +Poly/ML 5.2 or later.
     1.9 +
    1.10  * The Isabelle "emacs" tool provides a specific interface to invoke
    1.11  Proof General / Emacs, with more explicit failure if that is not
    1.12  installed (the old isabelle-interface script silently falls back on
     2.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 16 17:28:37 2008 +0200
     2.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 16 18:01:24 2008 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      ID:         $Id$
     2.5      Author:     Makarius
     2.6  
     2.7 -Multithreading in Poly/ML 5.1, 5.2 (cf. polyml/basis/Thread.sml).
     2.8 +Multithreading in Poly/ML 5.2 or later (cf. polyml/basis/Thread.sml).
     2.9  *)
    2.10  
    2.11  signature MULTITHREADING_POLYML =
    2.12 @@ -115,7 +115,7 @@
    2.13  
    2.14  (* system shell processes, with propagation of interrupts *)
    2.15  
    2.16 -fun system_out_threaded script = uninterruptible (fn restore_attributes => fn () =>
    2.17 +fun system_out script = uninterruptible (fn restore_attributes => fn () =>
    2.18    let
    2.19      val script_name = OS.FileSys.tmpName ();
    2.20      val _ = write_file script_name script;
    2.21 @@ -176,10 +176,6 @@
    2.22      val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
    2.23    in (output, rc) end) ();
    2.24  
    2.25 -val system_out =
    2.26 -  if ml_system = "polyml-5.1" then system_out  (*signals not propagated from root thread!*)
    2.27 -  else system_out_threaded;
    2.28 -
    2.29  
    2.30  (* critical section -- may be nested within the same thread *)
    2.31  
     3.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Sep 16 17:28:37 2008 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Sep 16 18:01:24 2008 +0200
     3.3 @@ -6,7 +6,6 @@
     3.4  
     3.5  open Thread;
     3.6  use "ML-Systems/polyml_common.ML";
     3.7 -use "ML-Systems/multithreading_polyml.ML";
     3.8  use "ML-Systems/polyml_old_compiler5.ML";
     3.9  
    3.10  val pointer_eq = PolyML.pointerEq;