# 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"