src/Pure/PIDE/markup.scala
changeset 55615 bf4bbe72f740
parent 55555 99409ccbe04a
child 55616 25a7a998852a
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Feb 19 21:38:44 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Feb 20 12:53:12 2014 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4        markup match {
     1.5          case Markup(ENTITY, props) =>
     1.6            (props, props) match {
     1.7 -            case (Kind(kind), Name(name)) => Some(kind, name)
     1.8 +            case (Kind(kind), Name(name)) => Some((kind, name))
     1.9              case _ => None
    1.10            }
    1.11          case _ => None
    1.12 @@ -87,8 +87,22 @@
    1.13  
    1.14    /* embedded languages */
    1.15  
    1.16 +  val SYMBOLS = "symbols"
    1.17 +  val Symbols = new Properties.Boolean(SYMBOLS)
    1.18 +
    1.19    val LANGUAGE = "language"
    1.20 -  val Language = new Markup_String(LANGUAGE, NAME)
    1.21 +  object Language
    1.22 +  {
    1.23 +    def unapply(markup: Markup): Option[(String, Boolean)] =
    1.24 +      markup match {
    1.25 +        case Markup(LANGUAGE, props) =>
    1.26 +          (props, props) match {
    1.27 +            case (Name(name), Symbols(symbols)) => Some((name, symbols))
    1.28 +            case _ => None
    1.29 +          }
    1.30 +        case _ => None
    1.31 +      }
    1.32 +  }
    1.33  
    1.34  
    1.35    /* external resources */