# HG changeset patch
# User wenzelm
# Date 1369147876 -7200
# Node ID 59cc8881e911d6458e0f37c3c43dd80f4cf0eb1e
# Parent  7679178b0aa5a16d737d1e797eb52926d9296691
tuned;

diff -r 7679178b0aa5 -r 59cc8881e911 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]] =