1.1 --- a/src/Pure/System/isabelle_process.ML	Mon Oct 25 21:23:09 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Oct 25 22:47:02 2010 +0200
     1.3 @@ -57,42 +57,33 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* message markup *)
     1.8 +(* message channels *)
     1.9  
    1.10  local
    1.11  
    1.12 -fun chunk s = string_of_int (size s) ^ "\n" ^ s;
    1.13 +fun chunk s = [string_of_int (size s), "\n", s];
    1.14  
    1.15  fun message _ _ _ "" = ()
    1.16 -  | message out_stream ch raw_props body =
    1.17 +  | message mbox ch raw_props body =
    1.18        let
    1.19          val robust_props = map (pairself YXML.escape_controls) raw_props;
    1.20          val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
    1.21 -      in TextIO.output (out_stream, chunk header ^ chunk body) (*atomic output!*) end;
    1.22 +      in Mailbox.send mbox (chunk header @ chunk body) end;
    1.23  
    1.24 -in
    1.25 -
    1.26 -fun standard_message out_stream with_serial ch body =
    1.27 -  message out_stream ch
    1.28 +fun standard_message mbox with_serial ch body =
    1.29 +  message mbox ch
    1.30      ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
    1.31        (Position.properties_of (Position.thread_data ()))) body;
    1.32  
    1.33 -fun init_message out_stream =
    1.34 -  message out_stream "A" [] (Session.welcome ());
    1.35 -
    1.36 -end;
    1.37 -
    1.38 -
    1.39 -(* channels *)
    1.40 -
    1.41 -local
    1.42 -
    1.43 -fun auto_flush stream =
    1.44 +fun message_output mbox out_stream =
    1.45    let
    1.46 -    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
    1.47 -    fun loop () =
    1.48 -      (OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
    1.49 -  in loop end;
    1.50 +    fun loop receive =
    1.51 +      (case receive mbox of
    1.52 +        SOME msg =>
    1.53 +         (List.app (fn s => TextIO.output (out_stream, s)) msg;
    1.54 +          loop (Mailbox.receive_timeout (Time.fromMilliseconds 20)))
    1.55 +      | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
    1.56 +  in fn () => loop (SOME o Mailbox.receive) end;
    1.57  
    1.58  in
    1.59  
    1.60 @@ -102,19 +93,22 @@
    1.61      val in_stream = TextIO.openIn in_fifo;
    1.62      val out_stream = TextIO.openOut out_fifo;
    1.63  
    1.64 -    val _ = Simple_Thread.fork false (auto_flush out_stream);
    1.65 -    val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
    1.66 -    val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
    1.67 +    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    1.68 +    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    1.69 +
    1.70 +    val mbox = Mailbox.create () : string list Mailbox.T;
    1.71 +    val _ = Simple_Thread.fork false (message_output mbox out_stream);
    1.72    in
    1.73 -    Output.Private_Hooks.status_fn := standard_message out_stream false "B";
    1.74 -    Output.Private_Hooks.report_fn := standard_message out_stream false "C";
    1.75 -    Output.Private_Hooks.writeln_fn := standard_message out_stream true "D";
    1.76 -    Output.Private_Hooks.tracing_fn := standard_message out_stream true "E";
    1.77 -    Output.Private_Hooks.warning_fn := standard_message out_stream true "F";
    1.78 -    Output.Private_Hooks.error_fn := standard_message out_stream true "G";
    1.79 +    Output.Private_Hooks.status_fn := standard_message mbox false "B";
    1.80 +    Output.Private_Hooks.report_fn := standard_message mbox false "C";
    1.81 +    Output.Private_Hooks.writeln_fn := standard_message mbox true "D";
    1.82 +    Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
    1.83 +    Output.Private_Hooks.warning_fn := standard_message mbox true "F";
    1.84 +    Output.Private_Hooks.error_fn := standard_message mbox true "G";
    1.85      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.86      Output.Private_Hooks.prompt_fn := ignore;
    1.87 -    (in_stream, out_stream)
    1.88 +    message mbox "A" [] (Session.welcome ());
    1.89 +    in_stream
    1.90    end;
    1.91  
    1.92  end;
    1.93 @@ -179,8 +173,7 @@
    1.94      val _ = Unsynchronized.change print_mode
    1.95        (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
    1.96  
    1.97 -    val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
    1.98 -    val _ = init_message out_stream;
    1.99 +    val in_stream = setup_channels in_fifo out_fifo;
   1.100      val _ = Keyword.status ();
   1.101      val _ = Output.status (Markup.markup Markup.ready "process ready");
   1.102    in loop in_stream end));