proper border (again) -- avoid NPE on Windows;
authorwenzelm
Wed Jul 31 22:15:17 2013 +0200 (2013-07-31)
changeset 528197ce3ebc268a1
parent 52818 76e9fbb7c080
child 52820 cb53b44b958c
proper border (again) -- avoid NPE on Windows;
uniform non-opaqueness -- relevant for Windows L&F;
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 21:53:33 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 22:15:17 2013 +0200
     1.3 @@ -113,12 +113,12 @@
     1.4    private object Node_Renderer_Component extends BorderPanel
     1.5    {
     1.6      opaque = false
     1.7 -    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
     1.8  
     1.9      var node_name = Document.Node.Name.empty
    1.10  
    1.11      var checkbox_geometry: Option[(Point, Dimension)] = None
    1.12      val checkbox = new CheckBox {
    1.13 +      opaque = false
    1.14        override def paintComponent(gfx: Graphics2D)
    1.15        {
    1.16          super.paintComponent(gfx)
    1.17 @@ -133,6 +133,7 @@
    1.18  
    1.19        override def paintComponent(gfx: Graphics2D)
    1.20        {
    1.21 +        border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    1.22          val size = peer.getSize()
    1.23          val insets = border.getBorderInsets(peer)
    1.24          val w = size.width - insets.left - insets.right