# HG changeset patch
# User wenzelm
# Date 1221580884 -7200
# Node ID d67ba23e0277b901a516fc158888b237297c5de3
# Parent  04fc1ba19f93405e1d9d6886927479e2811c3277
multithreading for Poly/ML 5.1 is no longer supported;

diff -r 04fc1ba19f93 -r d67ba23e0277 NEWS
--- a/NEWS	Tue Sep 16 17:28:37 2008 +0200
+++ b/NEWS	Tue Sep 16 18:01:24 2008 +0200
@@ -255,6 +255,9 @@
 
 *** System ***
 
+* Multithreading for Poly/ML 5.1 is no longer supported, only for
+Poly/ML 5.2 or later.
+
 * The Isabelle "emacs" tool provides a specific interface to invoke
 Proof General / Emacs, with more explicit failure if that is not
 installed (the old isabelle-interface script silently falls back on
diff -r 04fc1ba19f93 -r d67ba23e0277 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 16 17:28:37 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 16 18:01:24 2008 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Makarius
 
-Multithreading in Poly/ML 5.1, 5.2 (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML 5.2 or later (cf. polyml/basis/Thread.sml).
 *)
 
 signature MULTITHREADING_POLYML =
@@ -115,7 +115,7 @@
 
 (* system shell processes, with propagation of interrupts *)
 
-fun system_out_threaded script = uninterruptible (fn restore_attributes => fn () =>
+fun system_out script = uninterruptible (fn restore_attributes => fn () =>
   let
     val script_name = OS.FileSys.tmpName ();
     val _ = write_file script_name script;
@@ -176,10 +176,6 @@
     val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
   in (output, rc) end) ();
 
-val system_out =
-  if ml_system = "polyml-5.1" then system_out  (*signals not propagated from root thread!*)
-  else system_out_threaded;
-
 
 (* critical section -- may be nested within the same thread *)
 
diff -r 04fc1ba19f93 -r d67ba23e0277 src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Sep 16 17:28:37 2008 +0200
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Sep 16 18:01:24 2008 +0200
@@ -6,7 +6,6 @@
 
 open Thread;
 use "ML-Systems/polyml_common.ML";
-use "ML-Systems/multithreading_polyml.ML";
 use "ML-Systems/polyml_old_compiler5.ML";
 
 val pointer_eq = PolyML.pointerEq;