1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 16:40:17 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 21:41:48 2011 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  import java.lang.System
     1.6  import java.awt.{BorderLayout, Graphics2D, Insets}
     1.7 -import javax.swing.{JList, DefaultListCellRenderer, UIManager}
     1.8 +import javax.swing.{JList, DefaultListCellRenderer, BorderFactory}
     1.9  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.10  
    1.11  import org.gjt.sp.jedit.{View, jEdit}
    1.12 @@ -89,8 +89,7 @@
    1.13    private class Node_Renderer_Component extends Label
    1.14    {
    1.15      xAlignment = Alignment.Leading
    1.16 -    border = UIManager.getBorder("List.cellNoFocusBorder")
    1.17 -    val empty_insets = new Insets(0, 0, 0, 0)
    1.18 +    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    1.19  
    1.20      var node_name = Document.Node.Name.empty
    1.21      override def paintComponent(gfx: Graphics2D)
    1.22 @@ -98,7 +97,7 @@
    1.23        nodes_status.get(node_name) match {
    1.24          case Some(st) if st.total > 0 =>
    1.25            val size = peer.getSize()
    1.26 -          val insets = if (border == null) empty_insets else border.getBorderInsets(this.peer)
    1.27 +          val insets = border.getBorderInsets(this.peer)
    1.28            val w = size.width - insets.left - insets.right
    1.29            val h = size.height - insets.top - insets.bottom
    1.30            var end = size.width - insets.right
    1.31 @@ -130,7 +129,7 @@
    1.32        component.background = list.background
    1.33        component.foreground = list.foreground
    1.34        component.node_name = name
    1.35 -      component.text = name.theory + " "
    1.36 +      component.text = name.theory
    1.37      }
    1.38    }
    1.39    status.renderer = new Node_Renderer