changeset 37195 | e87d305a4490 |
parent 37194 | 825456e5db30 |
child 38230 | ed147003de4b |
--- a/src/Pure/General/markup.scala Sun May 30 15:27:49 2010 +0200 +++ b/src/Pure/General/markup.scala Sun May 30 16:00:13 2010 +0200 @@ -123,6 +123,7 @@ /* ML syntax */ val ML_KEYWORD = "ML_keyword" + val ML_DELIMITER = "ML_delimiter" val ML_IDENT = "ML_ident" val ML_TVAR = "ML_tvar" val ML_NUMERAL = "ML_numeral"