src/Pure/PIDE/markup.scala
changeset 55828 42ac3cfb89f6
parent 55765 ec7ca5388dea
child 55837 154855d9a564
     1.1 --- a/src/Pure/PIDE/markup.scala	Sat Mar 01 19:55:01 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Mar 01 22:46:31 2014 +0100
     1.3 @@ -94,6 +94,7 @@
     1.4  
     1.5    val Symbols = new Properties.Boolean("symbols")
     1.6    val Antiquotes = new Properties.Boolean("antiquotes")
     1.7 +  val Delimited = new Properties.Boolean("delimited")
     1.8  
     1.9    val LANGUAGE = "language"
    1.10    object Language
    1.11 @@ -101,12 +102,12 @@
    1.12      val ML = "ML"
    1.13      val UNKNOWN = "unknown"
    1.14  
    1.15 -    def unapply(markup: Markup): Option[(String, Boolean, Boolean)] =
    1.16 +    def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
    1.17        markup match {
    1.18          case Markup(LANGUAGE, props) =>
    1.19 -          (props, props, props) match {
    1.20 -            case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) =>
    1.21 -              Some((name, symbols, antiquotes))
    1.22 +          (props, props, props, props) match {
    1.23 +            case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
    1.24 +              Some((name, symbols, antiquotes, delimited))
    1.25              case _ => None
    1.26            }
    1.27          case _ => None