# HG changeset patch
# User wenzelm
# Date 1551299416 -3600
# Node ID e02e3763e7a445c2e578bcde67a57d772f88c9a8
# Parent  d28e8199dcb9f0ed83a18d3f8f1daee22305ccea
more compact representation: approx. factor 2;

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)));
 
diff -r d28e8199dcb9 -r e02e3763e7a4 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Feb 27 17:33:39 2019 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Feb 27 21:30:16 2019 +0100
@@ -16,7 +16,12 @@
     def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
       try {
         import XML.Decode._
-        Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text)))
+        def decode_upd(body: XML.Body): (Long, List[Long]) =
+          space_explode(',', string(body)).map(Value.Long.parse) match {
+            case a :: bs => (a, bs)
+            case _ => throw new XML.XML_Body(body)
+          }
+        Some(pair(long, list(decode_upd _))(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None