1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 21:41:48 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 21:53:07 2011 +0200
     1.3 @@ -86,8 +86,9 @@
     1.4  
     1.5    private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
     1.6  
     1.7 -  private class Node_Renderer_Component extends Label
     1.8 +  private object Node_Renderer_Component extends Label
     1.9    {
    1.10 +    opaque = false
    1.11      xAlignment = Alignment.Leading
    1.12      border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    1.13  
    1.14 @@ -118,18 +119,15 @@
    1.15      }
    1.16    }
    1.17  
    1.18 -  private class Node_Renderer extends
    1.19 -    ListView.AbstractRenderer[Document.Node.Name, Node_Renderer_Component](
    1.20 -      new Node_Renderer_Component)
    1.21 +  private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
    1.22    {
    1.23 -    def configure(list: ListView[_], isSelected: Boolean, focused: Boolean,
    1.24 -      name: Document.Node.Name, index: Int)
    1.25 +    def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
    1.26 +      name: Document.Node.Name, index: Int): Component =
    1.27      {
    1.28 -      component.opaque = false
    1.29 -      component.background = list.background
    1.30 -      component.foreground = list.foreground
    1.31 +      val component = Node_Renderer_Component
    1.32        component.node_name = name
    1.33        component.text = name.theory
    1.34 +      component
    1.35      }
    1.36    }
    1.37    status.renderer = new Node_Renderer