src/Pure/PIDE/isar_document.scala
changeset 44661 383c9d758a56
parent 44644 317e4962dd0f
child 44673 2fa51ac191bc
equal deleted inserted replaced
44660:90bab3febb6c 44661:383c9d758a56
    11 {
    11 {
    12   /* document editing */
    12   /* document editing */
    13 
    13 
    14   object Assign
    14   object Assign
    15   {
    15   {
    16     def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
    16     def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
    17       msg match {
    17       try {
    18         case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
    18         import XML.Decode._
    19           try {
    19         val body = YXML.parse_body(text)
    20             import XML.Decode._
    20         Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
    21             val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
    21       }
    22             Some(id, a)
    22       catch {
    23           }
    23         case ERROR(_) => None
    24           catch {
    24         case _: XML.XML_Atom => None
    25             case _: XML.XML_Atom => None
    25         case _: XML.XML_Body => None
    26             case _: XML.XML_Body => None
       
    27           }
       
    28         case _ => None
       
    29       }
    26       }
    30   }
    27   }
    31 
    28 
    32 
    29 
    33   /* toplevel transactions */
    30   /* toplevel transactions */