diff -r 825456e5db30 -r e87d305a4490 src/Pure/General/markup.scala
--- 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"