# HG changeset patch # User wenzelm # Date 1373731989 -7200 # Node ID 4cf6fbf1d9a13946a1bf3a77a403d2f23e3302b6 # Parent f45ab3e8211b884a00586e8b588f38bd48a2948f more rendering for information messages; diff -r f45ab3e8211b -r 4cf6fbf1d9a1 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sat Jul 13 17:05:22 2013 +0200 +++ b/src/Pure/PIDE/protocol.scala Sat Jul 13 18:13:09 2013 +0200 @@ -205,15 +205,18 @@ case _ => false } - def is_state(msg: XML.Tree): Boolean = + def is_writeln_markup(msg: XML.Tree, name: String): Boolean = msg match { case XML.Elem(Markup(Markup.WRITELN, _), - List(XML.Elem(Markup(Markup.STATE, _), _))) => true + List(XML.Elem(markup, _))) => markup.name == name case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), - List(XML.Elem(Markup(Markup.STATE, _), _))) => true + List(XML.Elem(markup, _))) => markup.name == name case _ => false } + def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE) + def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION) + def is_warning(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WARNING, _), _) => true diff -r f45ab3e8211b -r 4cf6fbf1d9a1 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Jul 13 17:05:22 2013 +0200 +++ b/src/Tools/jEdit/etc/options Sat Jul 13 18:13:09 2013 +0200 @@ -42,16 +42,17 @@ option bullet_color : string = "000000FF" option tooltip_color : string = "FFFFE9FF" option writeln_color : string = "C0C0C0FF" +option information_color : string = "C1DFEEFF" option warning_color : string = "FF8C00FF" option error_color : string = "B22222FF" option error1_color : string = "B2222232" option writeln_message_color : string = "F0F0F0FF" +option information_message_color : string = "C1DFEE32" option tracing_message_color : string = "F0F8FFFF" option warning_message_color : string = "EEE8AAFF" option error_message_color : string = "FFC1C1FF" option bad_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" -option information_color : string = "FFCC6632" option quoted_color : string = "8B8B8B19" option antiquoted_color : string = "FFC83219" option highlight_color : string = "50505032" diff -r f45ab3e8211b -r 4cf6fbf1d9a1 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Sat Jul 13 17:05:22 2013 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Sat Jul 13 18:13:09 2013 +0200 @@ -124,16 +124,17 @@ val bullet_color = color_value("bullet_color") val tooltip_color = color_value("tooltip_color") val writeln_color = color_value("writeln_color") + val information_color = color_value("information_color") val warning_color = color_value("warning_color") val error_color = color_value("error_color") val error1_color = color_value("error1_color") val writeln_message_color = color_value("writeln_message_color") + val information_message_color = color_value("information_message_color") val tracing_message_color = color_value("tracing_message_color") val warning_message_color = color_value("warning_message_color") 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") @@ -416,6 +417,7 @@ private val squiggly_colors = Map( Rendering.writeln_pri -> writeln_color, + Rendering.information_pri -> information_color, Rendering.warning_pri -> warning_color, Rendering.error_pri -> error_color) @@ -426,10 +428,12 @@ val results = snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ => { - case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) + case (pri, Text.Info(_, msg @ XML.Elem(Markup(name, _), _))) if name == Markup.WRITELN || name == Markup.WARNING || - name == Markup.ERROR => pri max Rendering.message_pri(name) + name == Markup.ERROR => + if (Protocol.is_information(msg)) pri max Rendering.information_pri + else pri max Rendering.message_pri(name) }) for { Text.Info(r, pri) <- results @@ -438,20 +442,24 @@ } - private val messages_include = - Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE) - private val message_colors = Map( Rendering.writeln_pri -> writeln_message_color, + Rendering.information_pri -> information_message_color, Rendering.tracing_pri -> tracing_message_color, Rendering.warning_pri -> warning_message_color, Rendering.error_pri -> error_message_color) + private val line_background_elements = + Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, + Markup.ERROR_MESSAGE, Markup.INFORMATION) + def line_background(range: Text.Range): Option[(Color, Boolean)] = { val results = - snapshot.cumulate_markup[Int](range, 0, Some(messages_include), _ => + snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ => { + case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) => + pri max Rendering.information_pri case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) if name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE || @@ -478,8 +486,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 + - Markup.INFORMATION ++ active_include + Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++ + active_include def background1(range: Text.Range): Stream[Text.Info[Color]] = { @@ -497,8 +505,6 @@ (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 =>