src/Pure/PIDE/markup.scala
changeset 66044 bd7516709051
parent 65937 fde7b5d209d5
child 66379 6392766f3c25
equal deleted inserted replaced
66043:f704c063e95d 66044:bd7516709051
   323 
   323 
   324 
   324 
   325   /* outer syntax */
   325   /* outer syntax */
   326 
   326 
   327   val COMMAND = "command"
   327   val COMMAND = "command"
       
   328   val KEYWORD = "keyword"
   328   val KEYWORD1 = "keyword1"
   329   val KEYWORD1 = "keyword1"
   329   val KEYWORD2 = "keyword2"
   330   val KEYWORD2 = "keyword2"
   330   val KEYWORD3 = "keyword3"
   331   val KEYWORD3 = "keyword3"
   331   val QUASI_KEYWORD = "quasi_keyword"
   332   val QUASI_KEYWORD = "quasi_keyword"
   332   val IMPROPER = "improper"
   333   val IMPROPER = "improper"