src/Pure/PIDE/markup.scala
changeset 63337 ae9330fdbc16
parent 62986 9d2fae6b31cc
child 63347 e344dc82f6c2
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Jun 21 11:03:24 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Jun 21 14:42:47 2016 +0200
     1.3 @@ -95,10 +95,9 @@
     1.4      def unapply(markup: Markup): Option[(String, String)] =
     1.5        markup match {
     1.6          case Markup(ENTITY, props) =>
     1.7 -          (props, props) match {
     1.8 -            case (Kind(kind), Name(name)) => Some((kind, name))
     1.9 -            case _ => None
    1.10 -          }
    1.11 +          val kind = Kind.unapply(props).getOrElse("")
    1.12 +          val name = Name.unapply(props).getOrElse("")
    1.13 +          Some((kind, name))
    1.14          case _ => None
    1.15        }
    1.16    }