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