separate color ranges by 1px to improve discernment of overall theory status;
authorwenzelm
Tue, 15 Jan 2013 12:45:19 +0100
changeset 50900 6d80709ab862
parent 50899 506ff6abfde0
child 50901 f4a6c360af35
separate color ranges by 1px to improve discernment of overall theory status;
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 _ =>
       }