src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Tue Jun 21 11:03:24 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Jun 21 14:42:47 2016 +0200
@@ -95,10 +95,9 @@
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) =>
-          (props, props) match {
-            case (Kind(kind), Name(name)) => Some((kind, name))
-            case _ => None
-          }
+          val kind = Kind.unapply(props).getOrElse("")
+          val name = Name.unapply(props).getOrElse("")
+          Some((kind, name))
         case _ => None
       }
   }