# HG changeset patch
# User wenzelm
# Date 1358250319 -3600
# Node ID 6d80709ab8620e3fd385e3069e8204f93ebce4da
# Parent  506ff6abfde0614b7de1c0ea5355d72641a03e3a
separate color ranges by 1px to improve discernment of overall theory status;

diff -r 506ff6abfde0 -r 6d80709ab862 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Jan 15 12:30:23 2013 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Jan 15 12:45:19 2013 +0100
@@ -86,22 +86,24 @@
     {
       nodes_status.get(node_name) match {
         case Some(st) if st.total > 0 =>
+          val colors = List(
+            (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
+            (st.running, PIDE.options.color_value("running_color")),
+            (st.warned, PIDE.options.color_value("warning_color")),
+            (st.failed, PIDE.options.color_value("error_color")))
+
           val size = peer.getSize()
           val insets = border.getBorderInsets(this.peer)
           val w = size.width - insets.left - insets.right
           val h = size.height - insets.top - insets.bottom
           var end = size.width - insets.right
-          for {
-            (n, color) <- List(
-              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
-              (st.running, PIDE.options.color_value("running_color")),
-              (st.warned, PIDE.options.color_value("warning_color")),
-              (st.failed, PIDE.options.color_value("error_color"))) }
+
+          for { (n, color) <- colors }
           {
             gfx.setColor(color)
-            val v = (n * w / st.total) max (if (n > 0) 4 else 0)
+            val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0)
             gfx.fillRect(end - v, insets.top, v, h)
-            end -= v
+            end = end - v - 1
           }
         case _ =>
       }