# 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)