src/Tools/jEdit/src/rendering.scala

--- a/src/Tools/jEdit/src/rendering.scala	Tue May 21 16:47:18 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue May 21 16:51:16 2013 +0200
@@ -554,7 +554,7 @@
       Markup.ML_STRING -> inner_quoted_color,
       Markup.ML_COMMENT -> inner_comment_color)
 
-  private val text_color_elements = Set.empty[String] ++ text_colors.keys
+  private val text_color_elements = text_colors.keySet
 
   def text_color(range: Text.Range, color: Color)
       : Stream[Text.Info[Color]] =