equal
deleted
inserted
replaced
85 val POSITION = "position" |
85 val POSITION = "position" |
86 |
86 |
87 |
87 |
88 /* embedded languages */ |
88 /* embedded languages */ |
89 |
89 |
90 val SYMBOLS = "symbols" |
90 val Symbols = new Properties.Boolean("symbols") |
91 val Symbols = new Properties.Boolean(SYMBOLS) |
91 val Antiquotes = new Properties.Boolean("antiquotes") |
92 |
92 |
93 val LANGUAGE = "language" |
93 val LANGUAGE = "language" |
94 object Language |
94 object Language |
95 { |
95 { |
96 val ML = "ML" |
96 val ML = "ML" |
97 val UNKNOWN = "unknown" |
97 val UNKNOWN = "unknown" |
98 |
98 |
99 def unapply(markup: Markup): Option[(String, Boolean)] = |
99 def unapply(markup: Markup): Option[(String, Boolean, Boolean)] = |
100 markup match { |
100 markup match { |
101 case Markup(LANGUAGE, props) => |
101 case Markup(LANGUAGE, props) => |
102 (props, props) match { |
102 (props, props, props) match { |
103 case (Name(name), Symbols(symbols)) => Some((name, symbols)) |
103 case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) => |
|
104 Some((name, symbols, antiquotes)) |
104 case _ => None |
105 case _ => None |
105 } |
106 } |
106 case _ => None |
107 case _ => None |
107 } |
108 } |
108 } |
109 } |