# HG changeset patch
# User wenzelm
# Date 1502718727 -7200
# Node ID 1f46b6693b56b8f2dc07712ff762a8c717154f1e
# Parent  e20ce089a14d2194ee39f790c9bfa30c9b39a239
tuned GUI;

diff -r e20ce089a14d -r 1f46b6693b56 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(