tuned GUI;
authorwenzelm
Mon Aug 14 13:58:38 2017 +0200 (23 months ago)
changeset 66412a8556be5be0b
parent 66411 72de7d59e2f7
child 66413 98afae4308f5
tuned GUI;
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 13:53:49 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 13:58:38 2017 +0200
     1.3 @@ -188,12 +188,13 @@
     1.4        val color =
     1.5          if (status == Overall_Node_Status.failed) PIDE.options.color_value("error_color")
     1.6          else label.foreground
     1.7 -      val thickness = if (status == Overall_Node_Status.pending) 1 else 3
     1.8 +      val thickness1 = if (status == Overall_Node_Status.pending) 1 else 3
     1.9 +      val thickness2 = 4 - thickness1
    1.10  
    1.11        label.border =
    1.12          BorderFactory.createCompoundBorder(
    1.13 -          BorderFactory.createLineBorder(color, thickness),
    1.14 -          BorderFactory.createEmptyBorder(3, 3, 3, 3))
    1.15 +          BorderFactory.createLineBorder(color, thickness1),
    1.16 +          BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
    1.17      }
    1.18  
    1.19      layout(checkbox) = BorderPanel.Position.West