init: more explicit protocol of open/remove rendezvous;
authorwenzelm
Fri, 29 Aug 2008 20:36:07 +0200
changeset 28062 f454a20c1ab1
parent 28061 5428435de53e
child 28063 3533485fc7b8
init: more explicit protocol of open/remove rendezvous;
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;