# HG changeset patch
# User wenzelm
# Date 1220996918 -7200
# Node ID 51ccf7fa6f185e85ad899509a8f79d67f867aacc
# Parent  4062882c7df3b37884228953723d82711c8f718d
auto_flush stdout, stderr as well;

diff -r 4062882c7df3 -r 51ccf7fa6f18 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Tue Sep 09 23:48:36 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Tue Sep 09 23:48:38 2008 +0200
@@ -98,6 +98,16 @@
 
 (* channels *)
 
+local
+
+fun auto_flush stream =
+  let
+    fun loop () =
+      (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
+  in loop end;
+
+in
+
 fun setup_channels out =
   let val out_stream =
     if out = "-" then TextIO.stdOut
@@ -107,12 +117,10 @@
         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);
+        val _ = Thread.fork (auto_flush TextIO.stdOut, Multithreading.no_interrupts);
       in out_stream end;
+    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;
@@ -125,6 +133,8 @@
     out_stream
   end;
 
+end;
+
 
 (* init *)