changeset 30615 | f1275196df16 |
parent 29522 | 793766d4c1b5 |
child 30702 | 274626e2b2dd |
--- a/src/Pure/General/markup.scala Fri Mar 20 20:22:13 2009 +0100 +++ b/src/Pure/General/markup.scala Fri Mar 20 21:32:12 2009 +0100 @@ -80,6 +80,18 @@ val DOC_ANTIQ = "doc_antiq" + /* ML syntax */ + + val ML_KEYWORD = "ML_keyword" + val ML_IDENT = "ML_ident" + val ML_TVAR = "ML_tvar" + val ML_NUMERAL = "ML_numeral" + val ML_CHAR = "ML_char" + val ML_STRING = "ML_string" + val ML_COMMENT = "ML_comment" + val ML_MALFORMED = "ML_malformed" + + /* outer syntax */ val KEYWORD_DECL = "keyword_decl"