# HG changeset patch
# User wenzelm
# Date 1220034967 -7200
# Node ID f454a20c1ab1c5d3125bf8c3968b0fb06e0e1a86
# Parent  5428435de53e7ac2f4cf2e66c073b92ceee9a391
init: more explicit protocol of open/remove rendezvous;

diff -r 5428435de53e -r f454a20c1ab1 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Fri Aug 29 20:36:05 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Fri Aug 29 20:36:07 2008 +0200
@@ -102,8 +102,11 @@
   let val out_stream =
     if out = "" orelse out = "-" then TextIO.stdOut
     else
-      let val path = File.platform_path (Path.explode out)
-      in TextIO.openOut path before OS.FileSys.remove path end;
+      let
+        val path = File.platform_path (Path.explode out);
+        val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
+        val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
+      in out_stream end;
   in
     Output.writeln_fn  := message out_stream "A" Markup.writelnN;
     Output.priority_fn := message out_stream "B" Markup.priorityN;