src/Pure/PIDE/markup.scala
changeset 56202 0a11d17eeeff
parent 55919 2eb8c13339a5
child 56278 2576d3a40ed6
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Mar 18 11:27:09 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Mar 18 12:25:17 2014 +0100
     1.3 @@ -216,6 +216,7 @@
     1.4    val KEYWORD2 = "keyword2"
     1.5    val KEYWORD3 = "keyword3"
     1.6    val QUASI_KEYWORD = "quasi_keyword"
     1.7 +  val IMPROPER = "improper"
     1.8    val OPERATOR = "operator"
     1.9    val STRING = "string"
    1.10    val ALTSTRING = "altstring"