less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
authorwenzelm
Tue May 21 16:47:18 2013 +0200 (2013-05-21 ago)
changeset 521017679178b0aa5
parent 52100 e58762f34639
child 52102 59cc8881e911
less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/etc/options	Tue May 21 13:22:47 2013 +0200
     1.2 +++ b/src/Tools/jEdit/etc/options	Tue May 21 16:47:18 2013 +0200
     1.3 @@ -52,6 +52,7 @@
     1.4  option bad_color : string = "FF6A6A64"
     1.5  option intensify_color : string = "FFCC6664"
     1.6  option quoted_color : string = "8B8B8B19"
     1.7 +option antiquoted_color : string = "FFC83219"
     1.8  option highlight_color : string = "50505032"
     1.9  option hyperlink_color : string = "000000FF"
    1.10  option active_color : string = "DCDCDCFF"
    1.11 @@ -69,6 +70,5 @@
    1.12  option inner_numeral_color : string = "FF0000FF"
    1.13  option inner_quoted_color : string = "D2691EFF"
    1.14  option inner_comment_color : string = "8B0000FF"
    1.15 -option antiquotation_color : string = "0000FFFF"
    1.16  option dynamic_color : string = "7BA428FF"
    1.17  
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue May 21 13:22:47 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue May 21 16:47:18 2013 +0200
     2.3 @@ -134,6 +134,7 @@
     2.4    val bad_color = color_value("bad_color")
     2.5    val intensify_color = color_value("intensify_color")
     2.6    val quoted_color = color_value("quoted_color")
     2.7 +  val antiquoted_color = color_value("antiquoted_color")
     2.8    val highlight_color = color_value("highlight_color")
     2.9    val hyperlink_color = color_value("hyperlink_color")
    2.10    val active_color = color_value("active_color")
    2.11 @@ -151,7 +152,6 @@
    2.12    val inner_numeral_color = color_value("inner_numeral_color")
    2.13    val inner_quoted_color = color_value("inner_quoted_color")
    2.14    val inner_comment_color = color_value("inner_comment_color")
    2.15 -  val antiquotation_color = color_value("antiquotation_color")
    2.16    val dynamic_color = color_value("dynamic_color")
    2.17  
    2.18  
    2.19 @@ -517,12 +517,16 @@
    2.20        })
    2.21  
    2.22  
    2.23 +  private val foreground_elements =
    2.24 +    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
    2.25 +
    2.26    def foreground(range: Text.Range): Stream[Text.Info[Color]] =
    2.27 -    snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
    2.28 +    snapshot.select_markup(range, Some(foreground_elements), _ =>
    2.29        {
    2.30          case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
    2.31          case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
    2.32          case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
    2.33 +        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => antiquoted_color
    2.34        })
    2.35  
    2.36  
    2.37 @@ -548,8 +552,7 @@
    2.38        Markup.ML_NUMERAL -> inner_numeral_color,
    2.39        Markup.ML_CHAR -> inner_quoted_color,
    2.40        Markup.ML_STRING -> inner_quoted_color,
    2.41 -      Markup.ML_COMMENT -> inner_comment_color,
    2.42 -      Markup.ANTIQ -> antiquotation_color)
    2.43 +      Markup.ML_COMMENT -> inner_comment_color)
    2.44  
    2.45    private val text_color_elements = Set.empty[String] ++ text_colors.keys
    2.46