# HG changeset patch
# User wenzelm
# Date 1502711918 -7200
# Node ID a8556be5be0bcf2311463b24071c43274abbd0cc
# Parent  72de7d59e2f7b4a7e8064539422b8c38cea67d36
tuned GUI;

diff -r 72de7d59e2f7 -r a8556be5be0b src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 13:53:49 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 13:58:38 2017 +0200
@@ -188,12 +188,13 @@
       val color =
         if (status == Overall_Node_Status.failed) PIDE.options.color_value("error_color")
         else label.foreground
-      val thickness = if (status == Overall_Node_Status.pending) 1 else 3
+      val thickness1 = if (status == Overall_Node_Status.pending) 1 else 3
+      val thickness2 = 4 - thickness1
 
       label.border =
         BorderFactory.createCompoundBorder(
-          BorderFactory.createLineBorder(color, thickness),
-          BorderFactory.createEmptyBorder(3, 3, 3, 3))
+          BorderFactory.createLineBorder(color, thickness1),
+          BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
     }
 
     layout(checkbox) = BorderPanel.Position.West