src/Pure/PIDE/markup.scala
changeset 55744 4a4e5686e091
parent 55694 a1184dfb8e00
child 55765 ec7ca5388dea
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 25 14:56:58 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 25 17:03:55 2014 +0100
     1.3 @@ -209,9 +209,11 @@
     1.4  
     1.5    /* outer syntax */
     1.6  
     1.7 -  val KEYWORD = "keyword"
     1.8 +  val COMMAND = "command"
     1.9 +
    1.10 +  val KEYWORD1 = "keyword1"
    1.11 +  val KEYWORD2 = "keyword2"
    1.12    val OPERATOR = "operator"
    1.13 -  val COMMAND = "command"
    1.14    val STRING = "string"
    1.15    val ALTSTRING = "altstring"
    1.16    val VERBATIM = "verbatim"
    1.17 @@ -219,9 +221,6 @@
    1.18    val COMMENT = "comment"
    1.19    val CONTROL = "control"
    1.20  
    1.21 -  val KEYWORD1 = "keyword1"
    1.22 -  val KEYWORD2 = "keyword2"
    1.23 -
    1.24  
    1.25    /* timing */
    1.26