src/Tools/jEdit/src/rendering.scala
changeset 55033 8e8243975860
parent 54702 3daeba5130f0
child 55316 885500f4aa6a
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Jan 17 20:51:36 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Jan 18 19:15:12 2014 +0100
     1.3 @@ -99,6 +99,7 @@
     1.4        Token.Kind.STRING -> LITERAL1,
     1.5        Token.Kind.ALT_STRING -> LITERAL2,
     1.6        Token.Kind.VERBATIM -> COMMENT3,
     1.7 +      Token.Kind.CARTOUCHE -> COMMENT4,
     1.8        Token.Kind.SPACE -> NULL,
     1.9        Token.Kind.COMMENT -> COMMENT1,
    1.10        Token.Kind.ERROR -> INVALID
    1.11 @@ -156,6 +157,7 @@
    1.12    val var_color = color_value("var_color")
    1.13    val inner_numeral_color = color_value("inner_numeral_color")
    1.14    val inner_quoted_color = color_value("inner_quoted_color")
    1.15 +  val inner_cartouche_color = color_value("inner_cartouche_color")
    1.16    val inner_comment_color = color_value("inner_comment_color")
    1.17    val dynamic_color = color_value("dynamic_color")
    1.18  
    1.19 @@ -593,6 +595,7 @@
    1.20        Markup.BOUND -> bound_color,
    1.21        Markup.VAR -> var_color,
    1.22        Markup.INNER_STRING -> inner_quoted_color,
    1.23 +      Markup.INNER_CARTOUCHE -> inner_cartouche_color,
    1.24        Markup.INNER_COMMENT -> inner_comment_color,
    1.25        Markup.DYNAMIC_FACT -> dynamic_color,
    1.26        Markup.ML_KEYWORD -> keyword1_color,