src/Pure/PIDE/markup.scala
changeset 66044 bd7516709051
parent 65937 fde7b5d209d5
child 66379 6392766f3c25
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Jun 08 21:17:13 2017 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Jun 08 23:04:07 2017 +0200
     1.3 @@ -325,6 +325,7 @@
     1.4    /* outer syntax */
     1.5  
     1.6    val COMMAND = "command"
     1.7 +  val KEYWORD = "keyword"
     1.8    val KEYWORD1 = "keyword1"
     1.9    val KEYWORD2 = "keyword2"
    1.10    val KEYWORD3 = "keyword3"