tuned;

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