tuned;
authorwenzelm
Tue May 21 16:51:16 2013 +0200 (2013-05-21 ago)
changeset 5210259cc8881e911
parent 52101 7679178b0aa5
child 52103 fb577a13abbd
tuned;
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue May 21 16:47:18 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue May 21 16:51:16 2013 +0200
     1.3 @@ -554,7 +554,7 @@
     1.4        Markup.ML_STRING -> inner_quoted_color,
     1.5        Markup.ML_COMMENT -> inner_comment_color)
     1.6  
     1.7 -  private val text_color_elements = Set.empty[String] ++ text_colors.keys
     1.8 +  private val text_color_elements = text_colors.keySet
     1.9  
    1.10    def text_color(range: Text.Range, color: Color)
    1.11        : Stream[Text.Info[Color]] =