# HG changeset patch
# User wenzelm
# Date 1551285219 -3600
# Node ID d28e8199dcb9f0ed83a18d3f8f1daee22305ccea
# Parent  b21ddfa7042b9a48956497420479169ea829345e
more scalable on 32-bit Poly/ML;

diff -r b21ddfa7042b -r d28e8199dcb9 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Feb 27 16:28:46 2019 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Feb 27 17:33:39 2019 +0100
@@ -117,10 +117,10 @@
 
             val _ =
               Output.protocol_message Markup.assign_update
-                [(new_id, assign_update) |>
+                ((new_id, assign_update) |>
                   let open XML.Encode
                   in pair int (list (pair int (list int))) end
-                  |> YXML.string_of_body];
+                  |> YXML.chunks_of_body);
           in Document.start_execution state' end)));
 
 val _ =
diff -r b21ddfa7042b -r d28e8199dcb9 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Wed Feb 27 16:28:46 2019 +0100
+++ b/src/Pure/PIDE/yxml.ML	Wed Feb 27 17:33:39 2019 +0100
@@ -23,6 +23,7 @@
   val output_markup: Markup.T -> string * string
   val buffer_body: XML.body -> Buffer.T -> Buffer.T
   val buffer: XML.tree -> Buffer.T -> Buffer.T
+  val chunks_of_body: XML.body -> string list
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val output_markup_elem: Markup.T -> (string * string) * string
@@ -78,6 +79,7 @@
       Buffer.add XYX
   | buffer (XML.Text s) = Buffer.add s
 
+fun chunks_of_body body = Buffer.empty |> buffer_body body |> Buffer.chunks;
 fun string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content;
 val string_of = string_of_body o single;