tuned GUI;
authorwenzelm
Mon, 14 Aug 2017 15:52:07 +0200
changeset 66417 1f46b6693b56
parent 66416 e20ce089a14d
child 66418 410b10ea405c
tuned GUI;
src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 15:40:48 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 15:52:07 2017 +0200
@@ -166,8 +166,8 @@
                 (st.failed, PIDE.options.color_value("error_color"))
               ).filter(_._1 > 0)
 
-            ((size.width - 1) /: segments)({ case (last, (n, color)) =>
-              val w = (n * ((size.width - 2) - segments.length) / st.total) max 4
+            ((size.width - 2) /: segments)({ case (last, (n, color)) =>
+              val w = (n * ((size.width - 4) - segments.length) / st.total) max 4
               paint_segment(last - w, w, color)
               last - w - 1
             })
@@ -188,8 +188,8 @@
       val color =
         if (status == Overall_Node_Status.failed) PIDE.options.color_value("error_color")
         else label.foreground
-      val thickness1 = if (status == Overall_Node_Status.pending) 1 else 3
-      val thickness2 = 4 - thickness1
+      val thickness1 = if (status == Overall_Node_Status.pending) 1 else 2
+      val thickness2 = 3 - thickness1
 
       label.border =
         BorderFactory.createCompoundBorder(