src/Pure/ML-Systems/multithreading_polyml.ML
changeset 28254 d67ba23e0277
parent 28169 356fc8734741
child 28398 9aa3216e5f31
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 16 17:28:37 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Sep 16 18:01:24 2008 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Multithreading in Poly/ML 5.1, 5.2 (cf. polyml/basis/Thread.sml).
     1.8 +Multithreading in Poly/ML 5.2 or later (cf. polyml/basis/Thread.sml).
     1.9  *)
    1.10  
    1.11  signature MULTITHREADING_POLYML =
    1.12 @@ -115,7 +115,7 @@
    1.13  
    1.14  (* system shell processes, with propagation of interrupts *)
    1.15  
    1.16 -fun system_out_threaded script = uninterruptible (fn restore_attributes => fn () =>
    1.17 +fun system_out script = uninterruptible (fn restore_attributes => fn () =>
    1.18    let
    1.19      val script_name = OS.FileSys.tmpName ();
    1.20      val _ = write_file script_name script;
    1.21 @@ -176,10 +176,6 @@
    1.22      val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
    1.23    in (output, rc) end) ();
    1.24  
    1.25 -val system_out =
    1.26 -  if ml_system = "polyml-5.1" then system_out  (*signals not propagated from root thread!*)
    1.27 -  else system_out_threaded;
    1.28 -
    1.29  
    1.30  (* critical section -- may be nested within the same thread *)
    1.31