# HG changeset patch
# User wenzelm
# Date 1516098603 -3600
# Node ID c98c6eb3dd4c0c6494e30ad9bf66e1917b3613b6
# Parent  1f4d167b6ac93f31a6df374d4472d8ba303f02d8
clarified markup;

diff -r 1f4d167b6ac9 -r c98c6eb3dd4c 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)