changeset 58900 | 1435cc20b022 |
parent 58592 | b0fff34d3247 |
child 58901 | 47809a811eba |
--- a/src/Tools/jEdit/src/rendering.scala Wed Nov 05 15:32:11 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Wed Nov 05 16:57:12 2014 +0100 @@ -85,7 +85,7 @@ } def token_markup(syntax: Outer_Syntax, token: Token): Byte = - if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse("")) + if (token.is_command) command_style(syntax.keywords.kind(token.content).getOrElse("")) else if (token.is_delimiter) JEditToken.OPERATOR else token_style(token.kind)