src/Pure/ML-Systems/multithreading_polyml.ML
changeset 26074 44c5419cd9f1
parent 25775 90525e67ede7
child 26083 abb3f8dd66dc
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Feb 15 17:36:21 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Feb 15 23:22:02 2008 +0100
     1.3 @@ -114,6 +114,46 @@
     1.4  end;
     1.5  
     1.6  
     1.7 +(* managed external processes -- with propagation of interrupts *)
     1.8 +
     1.9 +fun managed_process cmdline = uninterruptible (fn atts => fn () =>
    1.10 +  let
    1.11 +    val proc = Unix.execute (cmdline, []);
    1.12 +    val (proc_stdout, proc_stdin) = Unix.streamsOf proc;
    1.13 +    val _ = TextIO.closeOut proc_stdin;
    1.14 +
    1.15 +    (*finished state*)
    1.16 +    val finished = ref false;
    1.17 +    val finished_mutex = Mutex.mutex ();
    1.18 +    val finished_cond = ConditionVar.conditionVar ();
    1.19 +    fun signal_finished () =
    1.20 +      (Mutex.lock finished_mutex; finished := true; Mutex.unlock finished_mutex;
    1.21 +        ConditionVar.signal finished_cond);
    1.22 +
    1.23 +    val _ = Mutex.lock finished_mutex;
    1.24 +
    1.25 +    (*reader thread*)
    1.26 +    val buffer = ref [];
    1.27 +    fun reader () =
    1.28 +      (case Exn.capture TextIO.input proc_stdout of
    1.29 +        Exn.Exn Interrupt => ()
    1.30 +      | Exn.Exn _ => signal_finished ()
    1.31 +      | Exn.Result "" => signal_finished ()
    1.32 +      | Exn.Result txt => (change buffer (cons txt); reader ()));
    1.33 +    val reader_thread = Thread.fork (reader, []);
    1.34 +
    1.35 +    (*main thread*)
    1.36 +    val () =
    1.37 +      while not (! finished) do with_attributes atts (fn _ => fn () =>
    1.38 +        ((ConditionVar.waitUntil (finished_cond, finished_mutex, Time.now () + Time.fromSeconds 1); ())
    1.39 +          handle Interrupt => Unix.kill (proc, Posix.Signal.int))) ();  (* FIXME lock!?! *)
    1.40 +    val _ = Thread.interrupt reader_thread handle Thread _ => ();
    1.41 +
    1.42 +    val status = OS.Process.isSuccess (Unix.reap proc);
    1.43 +    val output = implode (rev (! buffer));
    1.44 +  in (output, status) end) ();
    1.45 +
    1.46 +
    1.47  (* critical section -- may be nested within the same thread *)
    1.48  
    1.49  local