src/Pure/System/isabelle_process.ML
changeset 39530 16adc476348f
parent 39528 c01d89d18ff0
child 39585 00be8711082f
     1.1 --- a/src/Pure/System/isabelle_process.ML	Sun Sep 19 23:38:34 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Sep 20 11:38:14 2010 +0200
     1.3 @@ -94,21 +94,14 @@
     1.4        (OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
     1.5    in loop end;
     1.6  
     1.7 -fun rendezvous f fifo =
     1.8 -  let
     1.9 -    val path = File.platform_path (Path.explode fifo);
    1.10 -    val result = f fifo;  (*should block until peer is ready*)
    1.11 -    val _ =
    1.12 -      if String.isSuffix "cygwin" ml_platform then ()  (*Cygwin 1.7: no proper blocking on open*)
    1.13 -      else OS.FileSys.remove path;  (*prevent future access*)
    1.14 -  in result end;
    1.15 -
    1.16  in
    1.17  
    1.18  fun setup_channels in_fifo out_fifo =
    1.19    let
    1.20 -    val in_stream = rendezvous TextIO.openIn in_fifo;
    1.21 -    val out_stream = rendezvous TextIO.openOut out_fifo;
    1.22 +    (*rendezvous*)
    1.23 +    val in_stream = TextIO.openIn in_fifo;
    1.24 +    val out_stream = TextIO.openOut out_fifo;
    1.25 +
    1.26      val _ = Simple_Thread.fork false (auto_flush out_stream);
    1.27      val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
    1.28      val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);