--- 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 *)