# 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;