src/Pure/System/message_channel.ML

--- a/src/Pure/System/message_channel.ML	Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/System/message_channel.ML	Mon Mar 31 10:28:08 2014 +0200
@@ -7,7 +7,7 @@
 signature MESSAGE_CHANNEL =
 sig
   type message
-  val message: string -> Properties.T -> string -> message
+  val message: string -> Properties.T -> string list -> message
   type T
   val send: T -> message -> unit
   val shutdown: T -> unit
@@ -21,13 +21,14 @@
 
 datatype message = Message of string list;
 
-fun chunk s = [string_of_int (size s), "\n", s];
+fun chunk ss =
+  string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss;
 
 fun message name raw_props body =
   let
     val robust_props = map (pairself YXML.embed_controls) raw_props;
     val header = YXML.string_of (XML.Elem ((name, robust_props), []));
-  in Message (chunk header @ chunk body) end;
+  in Message (chunk [header] @ chunk body) end;
 
 fun output_message channel (Message ss) =
   List.app (System_Channel.output channel) ss;
@@ -37,7 +38,7 @@
 
 fun flush channel = ignore (try System_Channel.flush channel);
 
-val flush_message = message Markup.protocolN Markup.flush "";
+val flush_message = message Markup.protocolN Markup.flush [];
 fun flush_output channel = (output_message channel flush_message; flush channel);