src/Pure/PIDE/markup.scala
changeset 59081 2ceb05ee0331
parent 58978 e42da880c61e
child 59112 e670969f34df
equal deleted inserted replaced
59080:611914621edb 59081:2ceb05ee0331
   259   val KEYWORD3 = "keyword3"
   259   val KEYWORD3 = "keyword3"
   260   val QUASI_KEYWORD = "quasi_keyword"
   260   val QUASI_KEYWORD = "quasi_keyword"
   261   val IMPROPER = "improper"
   261   val IMPROPER = "improper"
   262   val OPERATOR = "operator"
   262   val OPERATOR = "operator"
   263   val STRING = "string"
   263   val STRING = "string"
   264   val ALTSTRING = "altstring"
   264   val ALT_STRING = "alt_string"
   265   val VERBATIM = "verbatim"
   265   val VERBATIM = "verbatim"
   266   val CARTOUCHE = "cartouche"
   266   val CARTOUCHE = "cartouche"
   267   val COMMENT = "comment"
   267   val COMMENT = "comment"
   268 
   268 
   269 
   269