src/Pure/ML-Systems/multithreading_polyml.ML
changeset 26221 e557c20158e2
parent 26098 b59d33f73aed
child 26254 3def1a1fea4e
equal deleted inserted replaced
26220:d34b68c21f9a 26221:e557c20158e2
   120 end;
   120 end;
   121 
   121 
   122 
   122 
   123 (* system shell processes, with propagation of interrupts *)
   123 (* system shell processes, with propagation of interrupts *)
   124 
   124 
   125 fun system_out script = uninterruptible (fn restore_attributes => fn () =>
   125 fun system_out_threaded script = uninterruptible (fn restore_attributes => fn () =>
   126   let
   126   let
   127     val script_name = OS.FileSys.tmpName ();
   127     val script_name = OS.FileSys.tmpName ();
   128     val _ = write_file script_name script;
   128     val _ = write_file script_name script;
   129 
   129 
   130     val pid_name = OS.FileSys.tmpName ();
   130     val pid_name = OS.FileSys.tmpName ();
   180     val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
   180     val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
   181     val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   181     val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   182     val _ = Thread.interrupt system_thread handle Thread _ => ();
   182     val _ = Thread.interrupt system_thread handle Thread _ => ();
   183     val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
   183     val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
   184   in (output, rc) end) ();
   184   in (output, rc) end) ();
       
   185 
       
   186 val system_out =
       
   187   if ml_system = "polyml-5.1" then system_out  (*signals not propagated from root thread!*)
       
   188   else system_out_threaded;
   185 
   189 
   186 
   190 
   187 (* critical section -- may be nested within the same thread *)
   191 (* critical section -- may be nested within the same thread *)
   188 
   192 
   189 local
   193 local