init: more explicit protocol of open/remove rendezvous;
authorwenzelm
Fri Aug 29 20:36:07 2008 +0200 (2008-08-29)
changeset 28062f454a20c1ab1
parent 28061 5428435de53e
child 28063 3533485fc7b8
init: more explicit protocol of open/remove rendezvous;
src/Pure/Tools/isabelle_process.ML
     1.1 --- a/src/Pure/Tools/isabelle_process.ML	Fri Aug 29 20:36:05 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.ML	Fri Aug 29 20:36:07 2008 +0200
     1.3 @@ -102,8 +102,11 @@
     1.4    let val out_stream =
     1.5      if out = "" orelse out = "-" then TextIO.stdOut
     1.6      else
     1.7 -      let val path = File.platform_path (Path.explode out)
     1.8 -      in TextIO.openOut path before OS.FileSys.remove path end;
     1.9 +      let
    1.10 +        val path = File.platform_path (Path.explode out);
    1.11 +        val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
    1.12 +        val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
    1.13 +      in out_stream end;
    1.14    in
    1.15      Output.writeln_fn  := message out_stream "A" Markup.writelnN;
    1.16      Output.priority_fn := message out_stream "B" Markup.priorityN;