more compact representation: approx. factor 2;
authorwenzelm
Wed Feb 27 21:30:16 2019 +0100 (7 weeks ago ago)
changeset 70027e02e3763e7a4
parent 70026 d28e8199dcb9
child 70028 a12d2eb58aca
more compact representation: approx. factor 2;
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/protocol.ML	Wed Feb 27 17:33:39 2019 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Feb 27 21:30:16 2019 +0100
     1.3 @@ -118,8 +118,11 @@
     1.4              val _ =
     1.5                Output.protocol_message Markup.assign_update
     1.6                  ((new_id, assign_update) |>
     1.7 -                  let open XML.Encode
     1.8 -                  in pair int (list (pair int (list int))) end
     1.9 +                  let
    1.10 +                    open XML.Encode;
    1.11 +                    fun encode_upd (a, bs) =
    1.12 +                      string (space_implode "," (map Value.print_int (a :: bs)));
    1.13 +                  in pair int (list encode_upd) end
    1.14                    |> YXML.chunks_of_body);
    1.15            in Document.start_execution state' end)));
    1.16  
     2.1 --- a/src/Pure/PIDE/protocol.scala	Wed Feb 27 17:33:39 2019 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Feb 27 21:30:16 2019 +0100
     2.3 @@ -16,7 +16,12 @@
     2.4      def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
     2.5        try {
     2.6          import XML.Decode._
     2.7 -        Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text)))
     2.8 +        def decode_upd(body: XML.Body): (Long, List[Long]) =
     2.9 +          space_explode(',', string(body)).map(Value.Long.parse) match {
    2.10 +            case a :: bs => (a, bs)
    2.11 +            case _ => throw new XML.XML_Body(body)
    2.12 +          }
    2.13 +        Some(pair(long, list(decode_upd _))(Symbol.decode_yxml(text)))
    2.14        }
    2.15        catch {
    2.16          case ERROR(_) => None