changeset 37194 | 825456e5db30 |
parent 37186 | 349e9223c685 |
child 37195 | e87d305a4490 |
--- a/src/Pure/General/markup.scala Sun May 30 14:21:35 2010 +0200 +++ b/src/Pure/General/markup.scala Sun May 30 15:27:49 2010 +0200 @@ -144,6 +144,7 @@ val COMMAND_DECL = "command_decl" val KEYWORD = "keyword" + val OPERATOR = "operator" val COMMAND = "command" val IDENT = "ident" val STRING = "string"