src/Tools/jEdit/src/rendering.scala
changeset 52643 34c29356930e
parent 52530 99dd8b4ef3fe
child 52644 cea207576f81
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 12:39:45 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 13:25:42 2013 +0200
     1.3 @@ -132,6 +132,7 @@
     1.4    val error_message_color = color_value("error_message_color")
     1.5    val bad_color = color_value("bad_color")
     1.6    val intensify_color = color_value("intensify_color")
     1.7 +  val information_color = color_value("information_color")
     1.8    val quoted_color = color_value("quoted_color")
     1.9    val antiquoted_color = color_value("antiquoted_color")
    1.10    val highlight_color = color_value("highlight_color")
    1.11 @@ -469,8 +470,8 @@
    1.12  
    1.13    private val background1_include =
    1.14      Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
    1.15 -      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
    1.16 -      active_include
    1.17 +      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
    1.18 +      Markup.INFORMATION ++ active_include
    1.19  
    1.20    def background1(range: Text.Range): Stream[Text.Info[Color]] =
    1.21    {
    1.22 @@ -488,6 +489,8 @@
    1.23                  (None, Some(bad_color))
    1.24                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    1.25                  (None, Some(intensify_color))
    1.26 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
    1.27 +                (None, Some(information_color))
    1.28                case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    1.29                  command_state.results.get(serial) match {
    1.30                    case Some(Protocol.Dialog_Result(res)) if res == result =>