# HG changeset patch
# User wenzelm
# Date 1572694784 -3600
# Node ID 2c17fa0f51871effa0dea007a40daf6d0d1c3eff
# Parent  ff11af12dfdd5354fe642f365839a14eb499bc8a
more direct output of XML material -- bypass Buffer.T;

diff -r ff11af12dfdd -r 2c17fa0f5187 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat Nov 02 12:33:38 2019 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sat Nov 02 12:39:44 2019 +0100
@@ -106,15 +106,15 @@
     fun message name props body =
       Message_Channel.send msg_channel (Message_Channel.message name props body);
 
-    fun standard_message props name body =
-      if forall (fn s => s = "") body then ()
+    fun standard_message props name ss =
+      if forall (fn s => s = "") ss then ()
       else
         let
           val props' =
             (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
               (false, SOME id') => props @ [(Markup.idN, id')]
             | _ => props);
-        in message name props' body end;
+        in message name props' (XML.blob ss) end;
   in
     Private_Output.status_fn := standard_message [] Markup.statusN;
     Private_Output.report_fn := standard_message [] Markup.reportN;
@@ -130,12 +130,13 @@
     Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
     Private_Output.error_message_fn :=
       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
-    Private_Output.system_message_fn := message Markup.systemN [];
+    Private_Output.system_message_fn :=
+      (fn ss => message Markup.systemN [] (XML.blob ss));
     Private_Output.protocol_message_fn :=
-      (fn props => fn body => message Markup.protocolN props (YXML.chunks_of_body body));
+      (fn props => fn body => message Markup.protocolN props body);
 
     Session.init_protocol_handlers ();
-    message Markup.initN [] [Session.welcome ()];
+    message Markup.initN [] [XML.Text (Session.welcome ())];
     msg_channel
   end;
 
diff -r ff11af12dfdd -r 2c17fa0f5187 src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Sat Nov 02 12:33:38 2019 +0100
+++ b/src/Pure/System/message_channel.ML	Sat Nov 02 12:39:44 2019 +0100
@@ -7,7 +7,7 @@
 signature MESSAGE_CHANNEL =
 sig
   type message
-  val message: string -> Properties.T -> string list -> message
+  val message: string -> Properties.T -> XML.body -> message
   type T
   val send: T -> message -> unit
   val shutdown: T -> unit
@@ -19,19 +19,20 @@
 
 (* message *)
 
-datatype message = Message of string list;
+datatype message = Message of XML.body;
 
-fun chunk ss =
-  string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss;
+fun body_size body = fold (YXML.traverse (Integer.add o size)) body 0;
+
+fun chunk body = XML.Text (string_of_int (body_size body) ^ "\n") :: body;
 
 fun message name raw_props body =
   let
     val robust_props = map (apply2 YXML.embed_controls) raw_props;
-    val header = YXML.string_of (XML.Elem ((name, robust_props), []));
+    val header = XML.Elem ((name, robust_props), []);
   in Message (chunk [header] @ chunk body) end;
 
-fun output_message stream (Message ss) =
-  List.app (File.output stream) ss;
+fun output_message stream (Message body) =
+  fold (YXML.traverse (fn s => fn () => File.output stream s)) body ();
 
 
 (* channel *)