src/Tools/jEdit/src/theories_dockable.scala
changeset 50900 6d80709ab862
parent 50895 3a1edaa0dc6d
child 51534 123bd97fcea1
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Jan 15 12:30:23 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Jan 15 12:45:19 2013 +0100
     1.3 @@ -86,22 +86,24 @@
     1.4      {
     1.5        nodes_status.get(node_name) match {
     1.6          case Some(st) if st.total > 0 =>
     1.7 +          val colors = List(
     1.8 +            (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
     1.9 +            (st.running, PIDE.options.color_value("running_color")),
    1.10 +            (st.warned, PIDE.options.color_value("warning_color")),
    1.11 +            (st.failed, PIDE.options.color_value("error_color")))
    1.12 +
    1.13            val size = peer.getSize()
    1.14            val insets = border.getBorderInsets(this.peer)
    1.15            val w = size.width - insets.left - insets.right
    1.16            val h = size.height - insets.top - insets.bottom
    1.17            var end = size.width - insets.right
    1.18 -          for {
    1.19 -            (n, color) <- List(
    1.20 -              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
    1.21 -              (st.running, PIDE.options.color_value("running_color")),
    1.22 -              (st.warned, PIDE.options.color_value("warning_color")),
    1.23 -              (st.failed, PIDE.options.color_value("error_color"))) }
    1.24 +
    1.25 +          for { (n, color) <- colors }
    1.26            {
    1.27              gfx.setColor(color)
    1.28 -            val v = (n * w / st.total) max (if (n > 0) 4 else 0)
    1.29 +            val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0)
    1.30              gfx.fillRect(end - v, insets.top, v, h)
    1.31 -            end -= v
    1.32 +            end = end - v - 1
    1.33            }
    1.34          case _ =>
    1.35        }