src/Tools/jEdit/src/rendering.scala
changeset 50895 3a1edaa0dc6d
parent 50715 8cfd585b9162
child 51496 cb677987b7e3
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Jan 14 22:33:53 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Jan 14 23:08:40 2013 +0100
     1.3 @@ -180,10 +180,10 @@
     1.4            ((Protocol.Status.init, 0) /: results) {
     1.5              case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
     1.6  
     1.7 -        if (pri == Rendering.warning_pri) Some(warning_color)
     1.8 +        if (status.is_running) Some(running_color)
     1.9 +        else if (pri == Rendering.warning_pri) Some(warning_color)
    1.10          else if (pri == Rendering.error_pri) Some(error_color)
    1.11          else if (status.is_unprocessed) Some(unprocessed_color)
    1.12 -        else if (status.is_running) Some(running_color)
    1.13          else if (status.is_failed) Some(error_color)
    1.14          else None
    1.15        }