# HG changeset patch
# User wenzelm
# Date 1221039397 -7200
# Node ID fbad2eb5be9eb76c8b8c85ef5c3f600ee5ac6ff9
# Parent  51ccf7fa6f185e85ad899509a8f79d67f867aacc
auto_flush: uniform block buffering for all output streams;

diff -r 51ccf7fa6f18 -r fbad2eb5be9e src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Tue Sep 09 23:48:38 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Wed Sep 10 11:36:37 2008 +0200
@@ -102,6 +102,7 @@
 
 fun auto_flush stream =
   let
+    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
     fun loop () =
       (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
   in loop end;
@@ -109,18 +110,18 @@
 in
 
 fun setup_channels out =
-  let val out_stream =
-    if out = "-" then TextIO.stdOut
-    else
-      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*)
-        val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream out_stream, IO.BLOCK_BUF);
-        val _ = Thread.fork (auto_flush TextIO.stdOut, Multithreading.no_interrupts);
-      in out_stream end;
+  let
+    val out_stream =
+      if out = "-" then TextIO.stdOut
+      else
+        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*)
+          val _ = Thread.fork (auto_flush TextIO.stdOut, Multithreading.no_interrupts);
+        in out_stream end;
+    val _ = Thread.fork (auto_flush out_stream, Multithreading.no_interrupts);
     val _ = Thread.fork (auto_flush TextIO.stdErr, Multithreading.no_interrupts);
-    val _ = Thread.fork (auto_flush out_stream, Multithreading.no_interrupts);
   in
     Output.writeln_fn  := message out_stream "A" Markup.writelnN;
     Output.priority_fn := message out_stream "B" Markup.priorityN;