src/Pure/PIDE/protocol.scala
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 */