# 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