diff -r f704c063e95d -r bd7516709051 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Jun 08 21:17:13 2017 +0200 +++ b/src/Pure/PIDE/markup.scala Thu Jun 08 23:04:07 2017 +0200 @@ -325,6 +325,7 @@ /* outer syntax */ val COMMAND = "command" + val KEYWORD = "keyword" val KEYWORD1 = "keyword1" val KEYWORD2 = "keyword2" val KEYWORD3 = "keyword3"