# HG changeset patch
# User wenzelm
# Date 1315296972 -7200
# Node ID 8f7b3a89fc15886a1729b2ab5b7168994125bdf6
# Parent  11a1290fd0acff3e96887bb5ec0860bfc3d36418
flush after Output.raw_message (and init message) for reduced latency of important protocol events;

diff -r 11a1290fd0ac -r 8f7b3a89fc15 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Sep 05 17:45:37 2011 -0700
+++ b/src/Pure/System/isabelle_process.ML	Tue Sep 06 10:16:12 2011 +0200
@@ -66,27 +66,29 @@
 
 fun chunk s = [string_of_int (size s), "\n", s];
 
-fun message mbox ch raw_props body =
+fun message do_flush mbox ch raw_props body =
   let
     val robust_props = map (pairself YXML.embed_controls) raw_props;
     val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
-  in Mailbox.send mbox (chunk header @ chunk body) end;
+  in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
 
 fun standard_message mbox opt_serial ch body =
   if body = "" then ()
   else
-    message mbox ch
+    message false mbox ch
       ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
         (Position.properties_of (Position.thread_data ()))) body;
 
 fun message_output mbox out_stream =
   let
+    fun flush () = ignore (try TextIO.flushOut out_stream);
     fun loop receive =
       (case receive mbox of
-        SOME msg =>
+        SOME (msg, do_flush) =>
          (List.app (fn s => TextIO.output (out_stream, s)) msg;
+          if do_flush then flush () else ();
           loop (Mailbox.receive_timeout (seconds 0.02)))
-      | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
+      | NONE => (flush (); loop (SOME o Mailbox.receive)));
   in fn () => loop (SOME o Mailbox.receive) end;
 
 in
@@ -100,7 +102,7 @@
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
 
-    val mbox = Mailbox.create () : string list Mailbox.T;
+    val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
     val _ = Simple_Thread.fork false (message_output mbox out_stream);
   in
     Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
@@ -109,10 +111,10 @@
     Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
     Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
     Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
-    Output.Private_Hooks.raw_message_fn := message mbox "H";
+    Output.Private_Hooks.raw_message_fn := message true mbox "H";
     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     Output.Private_Hooks.prompt_fn := ignore;
-    message mbox "A" [] (Session.welcome ());
+    message true mbox "A" [] (Session.welcome ());
     in_stream
   end;