--- a/src/Tools/jEdit/src/rendering.scala Sat Jul 13 12:39:45 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Sat Jul 13 13:25:42 2013 +0200
@@ -132,6 +132,7 @@
val error_message_color = color_value("error_message_color")
val bad_color = color_value("bad_color")
val intensify_color = color_value("intensify_color")
+ val information_color = color_value("information_color")
val quoted_color = color_value("quoted_color")
val antiquoted_color = color_value("antiquoted_color")
val highlight_color = color_value("highlight_color")
@@ -469,8 +470,8 @@
private val background1_include =
Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
- Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
- active_include
+ Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
+ Markup.INFORMATION ++ active_include
def background1(range: Text.Range): Stream[Text.Info[Color]] =
{
@@ -488,6 +489,8 @@
(None, Some(bad_color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
(None, Some(intensify_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
+ (None, Some(information_color))
case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
command_state.results.get(serial) match {
case Some(Protocol.Dialog_Result(res)) if res == result =>