src/Pure/PIDE/protocol.scala
changeset 70284 3e17c3a5fd39
parent 69849 09f200c658ed
child 70638 f164cec7ac22
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sun May 19 14:14:56 2019 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sun May 19 18:10:45 2019 +0200
     1.3 @@ -13,7 +13,9 @@
     1.4  
     1.5    object Assign_Update
     1.6    {
     1.7 -    def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
     1.8 +    def unapply(text: String)
     1.9 +      : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
    1.10 +    {
    1.11        try {
    1.12          import XML.Decode._
    1.13          def decode_upd(body: XML.Body): (Long, List[Long]) =
    1.14 @@ -21,12 +23,13 @@
    1.15              case a :: bs => (a, bs)
    1.16              case _ => throw new XML.XML_Body(body)
    1.17            }
    1.18 -        Some(pair(long, list(decode_upd _))(Symbol.decode_yxml(text)))
    1.19 +        Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
    1.20        }
    1.21        catch {
    1.22          case ERROR(_) => None
    1.23          case _: XML.Error => None
    1.24        }
    1.25 +    }
    1.26    }
    1.27  
    1.28    object Removed