# HG changeset patch
# User wenzelm
# Date 1316370368 -7200
# Node ID ad5883642a8374be63d78f0f2d74aa18ec28fd32
# Parent  68b990e950b18ef7094f47683d7f0af1e1274d08
more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);

diff -r 68b990e950b1 -r ad5883642a83 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sun Sep 18 19:49:35 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Sep 18 20:26:08 2011 +0200
@@ -15,7 +15,7 @@
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 import java.lang.System
-import java.awt.{BorderLayout, Graphics2D}
+import java.awt.{BorderLayout, Graphics2D, Insets}
 import javax.swing.{JList, DefaultListCellRenderer, UIManager}
 import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
@@ -90,6 +90,7 @@
   {
     xAlignment = Alignment.Leading
     border = UIManager.getBorder("List.cellNoFocusBorder")
+    val empty_insets = new Insets(0, 0, 0, 0)
 
     var node_name = Document.Node.Name.empty
     override def paintComponent(gfx: Graphics2D)
@@ -97,7 +98,7 @@
       nodes_status.get(node_name) match {
         case Some(st) if st.total > 0 =>
           val size = peer.getSize()
-          val insets = border.getBorderInsets(this.peer)
+          val insets = if (border == null) empty_insets else border.getBorderInsets(this.peer)
           val w = size.width - insets.left - insets.right
           val h = size.height - insets.top - insets.bottom
           var end = size.width - insets.right