src/Pure/PIDE/markup.scala
changeset 55505 2a1ca7f6607b
parent 55390 36550a4eac5e
child 55526 39708e59f4b0
--- a/src/Pure/PIDE/markup.scala	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Feb 15 18:28:18 2014 +0100
@@ -169,7 +169,9 @@
 
   /* ML syntax */
 
-  val ML_KEYWORD = "ML_keyword"
+  val ML_KEYWORD1 = "ML_keyword1"
+  val ML_KEYWORD2 = "ML_keyword2"
+  val ML_KEYWORD3 = "ML_keyword3"
   val ML_DELIMITER = "ML_delimiter"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"