tuned GUI;
authorwenzelm
Mon, 14 Aug 2017 13:58:38 +0200
changeset 66412 a8556be5be0b
parent 66411 72de7d59e2f7
child 66413 98afae4308f5
tuned GUI;
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