# HG changeset patch
# User wenzelm
# Date 1375301717 -7200
# Node ID 7ce3ebc268a10f030ba1acc2ebacc3c1f79d017e
# Parent  76e9fbb7c0801c70318a57f94144809489e28712
proper border (again) -- avoid NPE on Windows;
uniform non-opaqueness -- relevant for Windows L&F;

diff -r 76e9fbb7c080 -r 7ce3ebc268a1 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