changeset 47542 | 26d0a76fef0a |
parent 47395 | e6261a493f04 |
child 48705 | dd32321d6eef |
--- a/src/Pure/PIDE/protocol.scala Wed Apr 18 18:31:48 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Wed Apr 18 20:22:44 2012 +0200 @@ -154,6 +154,15 @@ case _ => false } + object Sendback + { + def unapply(msg: Any): Option[XML.Body] = + msg match { + case XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), body) => Some(body) + case _ => None + } + } + /* reported positions */