# HG changeset patch # User wenzelm # Date 1355577997 -3600 # Node ID ebd75dfaab73999ea98ff8de0f309199775c0c66 # Parent 1b01a57d27499fd86939788160742ac5a8cf3898 tuned; diff -r 1b01a57d2749 -r ebd75dfaab73 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Sat Dec 15 13:14:55 2012 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sat Dec 15 14:26:37 2012 +0100 @@ -158,16 +158,18 @@ val overview_limit = options.int("jedit_text_overview_limit") + private val overview_include = Protocol.command_status_markup + Markup.WARNING + Markup.ERROR + def overview_color(range: Text.Range): Option[Color] = { if (snapshot.is_outdated) None else { val results = snapshot.cumulate_markup[(Protocol.Status, Int)]( - range, (Protocol.Status.init, 0), - Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR), _ => + range, (Protocol.Status.init, 0), Some(overview_include), _ => { - case ((status, pri), Text.Info(_, XML.Elem(markup, _))) => + case ((status, pri), Text.Info(_, XML.Elem(markup, _))) + if overview_include(markup.name) => if (markup.name == Markup.WARNING || markup.name == Markup.ERROR) (status, pri max Rendering.message_pri(markup.name)) else (Protocol.command_status(status, markup), pri)