src/Tools/jEdit/src/jedit_rendering.scala

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 16 11:27:52 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 16 11:30:03 2018 +0100
@@ -68,7 +68,6 @@
 
   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
     if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
-    else if (token.is_keyword && token.source == Symbol.comment_decoded) JEditToken.NULL
     else if (token.is_delimiter) JEditToken.OPERATOR
     else token_style(token.kind)