flush after Output.raw_message (and init message) for reduced latency of important protocol events;
authorwenzelm
Tue Sep 06 10:16:12 2011 +0200 (2011-09-06 ago)
changeset 447318f7b3a89fc15
parent 44730 11a1290fd0ac
child 44732 c58b69d888ac
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/System/isabelle_process.ML	Mon Sep 05 17:45:37 2011 -0700
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Sep 06 10:16:12 2011 +0200
     1.3 @@ -66,27 +66,29 @@
     1.4  
     1.5  fun chunk s = [string_of_int (size s), "\n", s];
     1.6  
     1.7 -fun message mbox ch raw_props body =
     1.8 +fun message do_flush mbox ch raw_props body =
     1.9    let
    1.10      val robust_props = map (pairself YXML.embed_controls) raw_props;
    1.11      val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
    1.12 -  in Mailbox.send mbox (chunk header @ chunk body) end;
    1.13 +  in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
    1.14  
    1.15  fun standard_message mbox opt_serial ch body =
    1.16    if body = "" then ()
    1.17    else
    1.18 -    message mbox ch
    1.19 +    message false mbox ch
    1.20        ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
    1.21          (Position.properties_of (Position.thread_data ()))) body;
    1.22  
    1.23  fun message_output mbox out_stream =
    1.24    let
    1.25 +    fun flush () = ignore (try TextIO.flushOut out_stream);
    1.26      fun loop receive =
    1.27        (case receive mbox of
    1.28 -        SOME msg =>
    1.29 +        SOME (msg, do_flush) =>
    1.30           (List.app (fn s => TextIO.output (out_stream, s)) msg;
    1.31 +          if do_flush then flush () else ();
    1.32            loop (Mailbox.receive_timeout (seconds 0.02)))
    1.33 -      | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
    1.34 +      | NONE => (flush (); loop (SOME o Mailbox.receive)));
    1.35    in fn () => loop (SOME o Mailbox.receive) end;
    1.36  
    1.37  in
    1.38 @@ -100,7 +102,7 @@
    1.39      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    1.40      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    1.41  
    1.42 -    val mbox = Mailbox.create () : string list Mailbox.T;
    1.43 +    val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
    1.44      val _ = Simple_Thread.fork false (message_output mbox out_stream);
    1.45    in
    1.46      Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    1.47 @@ -109,10 +111,10 @@
    1.48      Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
    1.49      Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
    1.50      Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
    1.51 -    Output.Private_Hooks.raw_message_fn := message mbox "H";
    1.52 +    Output.Private_Hooks.raw_message_fn := message true mbox "H";
    1.53      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.54      Output.Private_Hooks.prompt_fn := ignore;
    1.55 -    message mbox "A" [] (Session.welcome ());
    1.56 +    message true mbox "A" [] (Session.welcome ());
    1.57      in_stream
    1.58    end;
    1.59