src/Tools/jEdit/src/session_dockable.scala
changeset 44980 ad5883642a83
parent 44960 640c2b957f16
child 44981 2bec3b7514cf
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Sep 18 19:49:35 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Sep 18 20:26:08 2011 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  import scala.swing.event.{ButtonClicked, SelectionChanged}
     1.5  
     1.6  import java.lang.System
     1.7 -import java.awt.{BorderLayout, Graphics2D}
     1.8 +import java.awt.{BorderLayout, Graphics2D, Insets}
     1.9  import javax.swing.{JList, DefaultListCellRenderer, UIManager}
    1.10  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.11  
    1.12 @@ -90,6 +90,7 @@
    1.13    {
    1.14      xAlignment = Alignment.Leading
    1.15      border = UIManager.getBorder("List.cellNoFocusBorder")
    1.16 +    val empty_insets = new Insets(0, 0, 0, 0)
    1.17  
    1.18      var node_name = Document.Node.Name.empty
    1.19      override def paintComponent(gfx: Graphics2D)
    1.20 @@ -97,7 +98,7 @@
    1.21        nodes_status.get(node_name) match {
    1.22          case Some(st) if st.total > 0 =>
    1.23            val size = peer.getSize()
    1.24 -          val insets = border.getBorderInsets(this.peer)
    1.25 +          val insets = if (border == null) empty_insets else border.getBorderInsets(this.peer)
    1.26            val w = size.width - insets.left - insets.right
    1.27            val h = size.height - insets.top - insets.bottom
    1.28            var end = size.width - insets.right