tuned;
authorwenzelm
Sat Dec 15 14:26:37 2012 +0100 (2012-12-15 ago)
changeset 50547ebd75dfaab73
parent 50546 1b01a57d2749
child 50549 91c716c848c2
tuned;
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 13:14:55 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 14:26:37 2012 +0100
     1.3 @@ -158,16 +158,18 @@
     1.4  
     1.5    val overview_limit = options.int("jedit_text_overview_limit")
     1.6  
     1.7 +  private val overview_include = Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
     1.8 +
     1.9    def overview_color(range: Text.Range): Option[Color] =
    1.10    {
    1.11      if (snapshot.is_outdated) None
    1.12      else {
    1.13        val results =
    1.14          snapshot.cumulate_markup[(Protocol.Status, Int)](
    1.15 -          range, (Protocol.Status.init, 0),
    1.16 -          Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR), _ =>
    1.17 +          range, (Protocol.Status.init, 0), Some(overview_include), _ =>
    1.18            {
    1.19 -            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
    1.20 +            case ((status, pri), Text.Info(_, XML.Elem(markup, _)))
    1.21 +            if overview_include(markup.name) =>
    1.22                if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
    1.23                  (status, pri max Rendering.message_pri(markup.name))
    1.24                else (Protocol.command_status(status, markup), pri)