# HG changeset patch
# User wenzelm
# Date 1316461308 -7200
# Node ID 5450ab3c677ee6bf6de42dacb54ab889d424a97d
# Parent  33aa6da101d887cb5896c88b8ef079124b5c71fe
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);

diff -r 33aa6da101d8 -r 5450ab3c677e src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 16:40:17 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 21:41:48 2011 +0200
@@ -16,7 +16,7 @@
 
 import java.lang.System
 import java.awt.{BorderLayout, Graphics2D, Insets}
-import javax.swing.{JList, DefaultListCellRenderer, UIManager}
+import javax.swing.{JList, DefaultListCellRenderer, BorderFactory}
 import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
 import org.gjt.sp.jedit.{View, jEdit}
@@ -89,8 +89,7 @@
   private class Node_Renderer_Component extends Label
   {
     xAlignment = Alignment.Leading
-    border = UIManager.getBorder("List.cellNoFocusBorder")
-    val empty_insets = new Insets(0, 0, 0, 0)
+    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
 
     var node_name = Document.Node.Name.empty
     override def paintComponent(gfx: Graphics2D)
@@ -98,7 +97,7 @@
       nodes_status.get(node_name) match {
         case Some(st) if st.total > 0 =>
           val size = peer.getSize()
-          val insets = if (border == null) empty_insets else border.getBorderInsets(this.peer)
+          val insets = 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
@@ -130,7 +129,7 @@
       component.background = list.background
       component.foreground = list.foreground
       component.node_name = name
-      component.text = name.theory + " "
+      component.text = name.theory
     }
   }
   status.renderer = new Node_Renderer