src/Pure/PIDE/markup.scala
changeset 62806 de9bf8171626
parent 61864 3a5992c3410c
child 62986 9d2fae6b31cc
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri Apr 01 19:01:34 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri Apr 01 21:34:17 2016 +0200
     1.3 @@ -131,6 +131,15 @@
     1.4    /* expression */
     1.5  
     1.6    val EXPRESSION = "expression"
     1.7 +  object Expression
     1.8 +  {
     1.9 +    def unapply(markup: Markup): Option[String] =
    1.10 +      markup match {
    1.11 +        case Markup(EXPRESSION, Kind(kind)) => Some(kind)
    1.12 +        case Markup(EXPRESSION, _) => Some("")
    1.13 +        case _ => None
    1.14 +      }
    1.15 +  }
    1.16  
    1.17  
    1.18    /* citation */