src/Pure/PIDE/markup.scala
changeset 55666 cc350eb1087e
parent 55616 25a7a998852a
child 55672 5e25cc741ab9
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri Feb 21 23:42:43 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Feb 22 15:07:33 2014 +0100
     1.3 @@ -87,8 +87,8 @@
     1.4  
     1.5    /* embedded languages */
     1.6  
     1.7 -  val SYMBOLS = "symbols"
     1.8 -  val Symbols = new Properties.Boolean(SYMBOLS)
     1.9 +  val Symbols = new Properties.Boolean("symbols")
    1.10 +  val Antiquotes = new Properties.Boolean("antiquotes")
    1.11  
    1.12    val LANGUAGE = "language"
    1.13    object Language
    1.14 @@ -96,11 +96,12 @@
    1.15      val ML = "ML"
    1.16      val UNKNOWN = "unknown"
    1.17  
    1.18 -    def unapply(markup: Markup): Option[(String, Boolean)] =
    1.19 +    def unapply(markup: Markup): Option[(String, Boolean, Boolean)] =
    1.20        markup match {
    1.21          case Markup(LANGUAGE, props) =>
    1.22 -          (props, props) match {
    1.23 -            case (Name(name), Symbols(symbols)) => Some((name, symbols))
    1.24 +          (props, props, props) match {
    1.25 +            case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) =>
    1.26 +              Some((name, symbols, antiquotes))
    1.27              case _ => None
    1.28            }
    1.29          case _ => None