src/Pure/PIDE/protocol.scala
changeset 47542 26d0a76fef0a
parent 47395 e6261a493f04
child 48705 dd32321d6eef
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 18 18:31:48 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 18 20:22:44 2012 +0200
     1.3 @@ -154,6 +154,15 @@
     1.4        case _ => false
     1.5      }
     1.6  
     1.7 +  object Sendback
     1.8 +  {
     1.9 +    def unapply(msg: Any): Option[XML.Body] =
    1.10 +      msg match {
    1.11 +        case XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), body) => Some(body)
    1.12 +        case _ => None
    1.13 +      }
    1.14 +  }
    1.15 +
    1.16  
    1.17    /* reported positions */
    1.18