proper border (again) -- avoid NPE on Windows;
authorwenzelm
Wed, 31 Jul 2013 22:15:17 +0200
changeset 52819 7ce3ebc268a1
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
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 21:53:33 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 22:15:17 2013 +0200
@@ -113,12 +113,12 @@
   private object Node_Renderer_Component extends BorderPanel
   {
     opaque = false
-    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
 
     var node_name = Document.Node.Name.empty
 
     var checkbox_geometry: Option[(Point, Dimension)] = None
     val checkbox = new CheckBox {
+      opaque = false
       override def paintComponent(gfx: Graphics2D)
       {
         super.paintComponent(gfx)
@@ -133,6 +133,7 @@
 
       override def paintComponent(gfx: Graphics2D)
       {
+        border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
         val size = peer.getSize()
         val insets = border.getBorderInsets(peer)
         val w = size.width - insets.left - insets.right