src/Tools/jEdit/src/rendering.scala
changeset 52101 7679178b0aa5
parent 52081 29566b6810f7
child 52102 59cc8881e911
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue May 21 13:22:47 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue May 21 16:47:18 2013 +0200
     1.3 @@ -134,6 +134,7 @@
     1.4    val bad_color = color_value("bad_color")
     1.5    val intensify_color = color_value("intensify_color")
     1.6    val quoted_color = color_value("quoted_color")
     1.7 +  val antiquoted_color = color_value("antiquoted_color")
     1.8    val highlight_color = color_value("highlight_color")
     1.9    val hyperlink_color = color_value("hyperlink_color")
    1.10    val active_color = color_value("active_color")
    1.11 @@ -151,7 +152,6 @@
    1.12    val inner_numeral_color = color_value("inner_numeral_color")
    1.13    val inner_quoted_color = color_value("inner_quoted_color")
    1.14    val inner_comment_color = color_value("inner_comment_color")
    1.15 -  val antiquotation_color = color_value("antiquotation_color")
    1.16    val dynamic_color = color_value("dynamic_color")
    1.17  
    1.18  
    1.19 @@ -517,12 +517,16 @@
    1.20        })
    1.21  
    1.22  
    1.23 +  private val foreground_elements =
    1.24 +    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
    1.25 +
    1.26    def foreground(range: Text.Range): Stream[Text.Info[Color]] =
    1.27 -    snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
    1.28 +    snapshot.select_markup(range, Some(foreground_elements), _ =>
    1.29        {
    1.30          case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
    1.31          case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
    1.32          case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
    1.33 +        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => antiquoted_color
    1.34        })
    1.35  
    1.36  
    1.37 @@ -548,8 +552,7 @@
    1.38        Markup.ML_NUMERAL -> inner_numeral_color,
    1.39        Markup.ML_CHAR -> inner_quoted_color,
    1.40        Markup.ML_STRING -> inner_quoted_color,
    1.41 -      Markup.ML_COMMENT -> inner_comment_color,
    1.42 -      Markup.ANTIQ -> antiquotation_color)
    1.43 +      Markup.ML_COMMENT -> inner_comment_color)
    1.44  
    1.45    private val text_color_elements = Set.empty[String] ++ text_colors.keys
    1.46