system_out: threaded version does not work for 5.1;
authorwenzelm
Thu Mar 06 20:17:51 2008 +0100 (2008-03-06)
changeset 26221e557c20158e2
parent 26220 d34b68c21f9a
child 26222 edf6473ac9e9
system_out: threaded version does not work for 5.1;
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Mar 06 20:17:50 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Mar 06 20:17:51 2008 +0100
     1.3 @@ -122,7 +122,7 @@
     1.4  
     1.5  (* system shell processes, with propagation of interrupts *)
     1.6  
     1.7 -fun system_out script = uninterruptible (fn restore_attributes => fn () =>
     1.8 +fun system_out_threaded script = uninterruptible (fn restore_attributes => fn () =>
     1.9    let
    1.10      val script_name = OS.FileSys.tmpName ();
    1.11      val _ = write_file script_name script;
    1.12 @@ -183,6 +183,10 @@
    1.13      val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
    1.14    in (output, rc) end) ();
    1.15  
    1.16 +val system_out =
    1.17 +  if ml_system = "polyml-5.1" then system_out  (*signals not propagated from root thread!*)
    1.18 +  else system_out_threaded;
    1.19 +
    1.20  
    1.21  (* critical section -- may be nested within the same thread *)
    1.22