1.1 --- a/src/Pure/System/isabelle_process.ML	Tue Jul 30 19:53:06 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 30 21:22:37 2013 +0200
     1.3 @@ -33,7 +33,8 @@
     1.4  local
     1.5  
     1.6  val commands =
     1.7 -  Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table);
     1.8 +  Synchronized.var "Isabelle_Process.commands"
     1.9 +    (Symtab.empty: (string list -> unit) Symtab.table);
    1.10  
    1.11  in
    1.12  
    1.13 @@ -90,20 +91,7 @@
    1.14        end);
    1.15  
    1.16  
    1.17 -(* message channels *)
    1.18 -
    1.19 -local
    1.20 -
    1.21 -fun chunk s = [string_of_int (size s), "\n", s];
    1.22 -
    1.23 -fun message do_flush msg_channel name raw_props body =
    1.24 -  let
    1.25 -    val robust_props = map (pairself YXML.embed_controls) raw_props;
    1.26 -    val header = YXML.string_of (XML.Elem ((name, robust_props), []));
    1.27 -    val msg = chunk header @ chunk body;
    1.28 -  in Message_Channel.send msg_channel msg do_flush end;
    1.29 -
    1.30 -in
    1.31 +(* output channels *)
    1.32  
    1.33  fun init_channels channel =
    1.34    let
    1.35 @@ -112,10 +100,13 @@
    1.36  
    1.37      val msg_channel = Message_Channel.make channel;
    1.38  
    1.39 +    fun message name props body =
    1.40 +      Message_Channel.send msg_channel (Message_Channel.message name props body);
    1.41 +
    1.42      fun standard_message opt_serial name body =
    1.43        if body = "" then ()
    1.44        else
    1.45 -        message false msg_channel name
    1.46 +        message name
    1.47            ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
    1.48              (Position.properties_of (Position.thread_data ()))) body;
    1.49    in
    1.50 @@ -130,15 +121,13 @@
    1.51        (fn s => standard_message (SOME (serial ())) Markup.warningN s);
    1.52      Output.Private_Hooks.error_fn :=
    1.53        (fn (i, s) => standard_message (SOME i) Markup.errorN s);
    1.54 -    Output.Private_Hooks.protocol_message_fn := message true msg_channel Markup.protocolN;
    1.55 +    Output.Private_Hooks.protocol_message_fn := message Markup.protocolN;
    1.56      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.57      Output.Private_Hooks.prompt_fn := ignore;
    1.58 -    message true msg_channel Markup.initN [] (Session.welcome ());
    1.59 +    message Markup.initN [] (Session.welcome ());
    1.60      msg_channel
    1.61    end;
    1.62  
    1.63 -end;
    1.64 -
    1.65  
    1.66  (* protocol loop -- uninterruptible *)
    1.67