src/Pure/PIDE/protocol.ML
changeset 69845 d28e8199dcb9
parent 68381 2fd3a6d6ba2e
child 69846 e02e3763e7a4
--- 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 _ =