# HG changeset patch
# User wenzelm
# Date 1316461987 -7200
# Node ID 3aa261a3c7d6ff059ac2298a365a580b2ac8bd13
# Parent  5450ab3c677ee6bf6de42dacb54ab889d424a97d
tuned;

diff -r 5450ab3c677e -r 3aa261a3c7d6 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 21:41:48 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 21:53:07 2011 +0200
@@ -86,8 +86,9 @@
 
   private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
 
-  private class Node_Renderer_Component extends Label
+  private object Node_Renderer_Component extends Label
   {
+    opaque = false
     xAlignment = Alignment.Leading
     border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
 
@@ -118,18 +119,15 @@
     }
   }
 
-  private class Node_Renderer extends
-    ListView.AbstractRenderer[Document.Node.Name, Node_Renderer_Component](
-      new Node_Renderer_Component)
+  private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
   {
-    def configure(list: ListView[_], isSelected: Boolean, focused: Boolean,
-      name: Document.Node.Name, index: Int)
+    def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
+      name: Document.Node.Name, index: Int): Component =
     {
-      component.opaque = false
-      component.background = list.background
-      component.foreground = list.foreground
+      val component = Node_Renderer_Component
       component.node_name = name
       component.text = name.theory
+      component
     }
   }
   status.renderer = new Node_Renderer