# 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