author | wenzelm |
Fri, 20 Mar 2009 21:32:12 +0100 | |
changeset 30615 | f1275196df16 |
parent 30614 | 845bcfd3e9cd |
child 30616 | ac79f1bb5db3 |
--- 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"