src/Pure/PIDE/markup.scala
changeset 55919 2eb8c13339a5
parent 55914 c5b752d549e3
child 56202 0a11d17eeeff
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Mar 05 16:06:11 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Mar 05 16:13:24 2014 +0100
     1.3 @@ -215,6 +215,7 @@
     1.4    val KEYWORD1 = "keyword1"
     1.5    val KEYWORD2 = "keyword2"
     1.6    val KEYWORD3 = "keyword3"
     1.7 +  val QUASI_KEYWORD = "quasi_keyword"
     1.8    val OPERATOR = "operator"
     1.9    val STRING = "string"
    1.10    val ALTSTRING = "altstring"