diff -r d28e8199dcb9 -r e02e3763e7a4 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Feb 27 17:33:39 2019 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Feb 27 21:30:16 2019 +0100
@@ -118,8 +118,11 @@
             val _ =
               Output.protocol_message Markup.assign_update
                 ((new_id, assign_update) |>
-                  let open XML.Encode
-                  in pair int (list (pair int (list int))) end
+                  let
+                    open XML.Encode;
+                    fun encode_upd (a, bs) =
+                      string (space_implode "," (map Value.print_int (a :: bs)));
+                  in pair int (list encode_upd) end
                   |> YXML.chunks_of_body);
           in Document.start_execution state' end)));