# HG changeset patch # User wenzelm # Date 1220983074 -7200 # Node ID bfd7a87006761868443c03338103f05f4bab097c # Parent e98be9824b7d44e0fd1af3ebef2dc085606a51d8 out_stream: block-buffered, with separate autoflush thread (every 50ms); diff -r e98be9824b7d -r bfd7a8700676 src/Pure/Tools/isabelle_process.ML --- a/src/Pure/Tools/isabelle_process.ML Tue Sep 09 19:36:21 2008 +0200 +++ b/src/Pure/Tools/isabelle_process.ML Tue Sep 09 19:57:54 2008 +0200 @@ -71,7 +71,7 @@ | get_pos _ = NONE; fun output out_stream s = NAMED_CRITICAL "IO" (fn () => - (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n"); TextIO.flushOut out_stream)); + (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n"))); in @@ -106,6 +106,12 @@ 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*) + val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream out_stream, IO.BLOCK_BUF); + fun auto_flush () = + (OS.Process.sleep (Time.fromMilliseconds 50); + CRITICAL (fn () => TextIO.flushOut out_stream); + auto_flush ()); + val _ = Thread.fork (auto_flush, Multithreading.no_interrupts); in out_stream end; in Output.writeln_fn := message out_stream "A" Markup.writelnN;