equal
deleted
inserted
replaced
167 val TEXT_FOLD = "text_fold" |
167 val TEXT_FOLD = "text_fold" |
168 |
168 |
169 |
169 |
170 /* ML syntax */ |
170 /* ML syntax */ |
171 |
171 |
172 val ML_KEYWORD = "ML_keyword" |
172 val ML_KEYWORD1 = "ML_keyword1" |
|
173 val ML_KEYWORD2 = "ML_keyword2" |
|
174 val ML_KEYWORD3 = "ML_keyword3" |
173 val ML_DELIMITER = "ML_delimiter" |
175 val ML_DELIMITER = "ML_delimiter" |
174 val ML_TVAR = "ML_tvar" |
176 val ML_TVAR = "ML_tvar" |
175 val ML_NUMERAL = "ML_numeral" |
177 val ML_NUMERAL = "ML_numeral" |
176 val ML_CHAR = "ML_char" |
178 val ML_CHAR = "ML_char" |
177 val ML_STRING = "ML_string" |
179 val ML_STRING = "ML_string" |