src/Tools/jEdit/src/rendering.scala
changeset 55526 39708e59f4b0
parent 55514 8ef781e282d9
child 55547 4a9f76263ece
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 21:33:28 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 17 11:14:26 2014 +0100
     1.3 @@ -177,6 +177,7 @@
     1.4    val intensify_color = color_value("intensify_color")
     1.5    val quoted_color = color_value("quoted_color")
     1.6    val antiquoted_color = color_value("antiquoted_color")
     1.7 +  val antiquote_color = color_value("antiquote_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 @@ -606,13 +607,13 @@
    1.12  
    1.13  
    1.14    private val foreground_include =
    1.15 -    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQ)
    1.16 +    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
    1.17  
    1.18    def foreground(range: Text.Range): List[Text.Info[Color]] =
    1.19      snapshot.select_markup(range, Some(foreground_include), _ =>
    1.20        {
    1.21          case Text.Info(_, elem) =>
    1.22 -          if (elem.name == Markup.ANTIQ) Some(antiquoted_color)
    1.23 +          if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color)
    1.24            else if (foreground_include.contains(elem.name)) Some(quoted_color)
    1.25            else None
    1.26        })
    1.27 @@ -637,6 +638,7 @@
    1.28        Markup.INNER_CARTOUCHE -> inner_cartouche_color,
    1.29        Markup.INNER_COMMENT -> inner_comment_color,
    1.30        Markup.DYNAMIC_FACT -> dynamic_color,
    1.31 +      Markup.ANTIQUOTE -> antiquote_color,
    1.32        Markup.ML_KEYWORD1 -> keyword1_color,
    1.33        Markup.ML_KEYWORD2 -> keyword2_color,
    1.34        Markup.ML_KEYWORD3 -> keyword3_color,