src/Pure/PIDE/isar_document.scala
changeset 44676 7de87f1ae965
parent 44673 2fa51ac191bc
child 44866 0eb8284a64bd
equal deleted inserted replaced
44675:f665a5d35a3d 44676:7de87f1ae965
    16     def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
    16     def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
    17       try {
    17       try {
    18         import XML.Decode._
    18         import XML.Decode._
    19         val body = YXML.parse_body(text)
    19         val body = YXML.parse_body(text)
    20         Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
    20         Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
       
    21       }
       
    22       catch {
       
    23         case ERROR(_) => None
       
    24         case _: XML.XML_Atom => None
       
    25         case _: XML.XML_Body => None
       
    26       }
       
    27   }
       
    28 
       
    29   object Removed
       
    30   {
       
    31     def unapply(text: String): Option[List[Document.Version_ID]] =
       
    32       try {
       
    33         import XML.Decode._
       
    34         Some(list(long)(YXML.parse_body(text)))
    21       }
    35       }
    22       catch {
    36       catch {
    23         case ERROR(_) => None
    37         case ERROR(_) => None
    24         case _: XML.XML_Atom => None
    38         case _: XML.XML_Atom => None
    25         case _: XML.XML_Body => None
    39         case _: XML.XML_Body => None