# HG changeset patch # User wenzelm # Date 1237581132 -3600 # Node ID f1275196df162808b627848ef0a2bacbdf6748d8 # Parent 845bcfd3e9cd75bf38720c6ea80c99b7157672cc added ML syntax markup; diff -r 845bcfd3e9cd -r f1275196df16 src/Pure/General/markup.scala --- 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"