# HG changeset patch
# User wenzelm
# Date 1348844393 -7200
# Node ID e5c16ccc5a878338d81a7af28f2fa45ddf4c3c92
# Parent  21ae8500d2618aea75d1996f22fedbd09a7ddb65
eliminated dead code;

diff -r 21ae8500d261 -r e5c16ccc5a87 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Sep 28 16:51:58 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Sep 28 16:59:53 2012 +0200
@@ -166,15 +166,6 @@
       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 */