proper border (again) -- avoid NPE on Windows;
uniform non-opaqueness -- relevant for Windows L&F;
--- 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