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 _ =