src/Tools/jEdit/src/session_dockable.scala

 
 
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
   ScrollPane, TabbedPane, Component, Swing}
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 import java.lang.System
-import java.awt.{BorderLayout, Graphics}
-import javax.swing.{JList, DefaultListCellRenderer}
+import java.awt.{BorderLayout, Graphics2D}
+import javax.swing.{JList, DefaultListCellRenderer, UIManager}
 import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
 import org.gjt.sp.jedit.{View, jEdit}
 
 

   /* main tabs */
 
   private val readme = new HTML_Panel("SansSerif", 14)
   readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
 
-  val status = new ListView(Nil: List[String])
+  val status = new ListView(Nil: List[Document.Node.Name])
   status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
   status.selection.intervalMode = ListView.IntervalMode.Single
 
   private val syslog = new TextArea(Isabelle.session.syslog())
 

 
   /* component state -- owned by Swing thread */
 
   private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
 
-  val node_renderer = new DefaultListCellRenderer
+  private class Node_Renderer_Component extends Label
   {
-    override def paintComponent(gfx: Graphics)
+    xAlignment = Alignment.Leading
+    border = UIManager.getBorder("List.cellNoFocusBorder")
+
+    var node_name = Document.Node.Name.empty
+    override def paintComponent(gfx: Graphics2D)
     {
-      nodes_status.get(Document.Node.Name(getText, "", "")) match {
+      nodes_status.get(node_name) match {
         case Some(st) if st.total > 0 =>
           val w = getWidth
           val h = getHeight
           var end = w
           for {

       }
       super.paintComponent(gfx)
     }
   }
 
-  status.peer.setCellRenderer(node_renderer)
+  private class Node_Renderer extends
+    ListView.AbstractRenderer[Document.Node.Name, Node_Renderer_Component](
+      new Node_Renderer_Component)
+  {
+    def configure(list: ListView[_], isSelected: Boolean, focused: Boolean,
+      name: Document.Node.Name, index: Int)
+    {
+      component.opaque = false
+      component.node_name = name
+      component.text = name.theory
+    }
+  }
+  status.renderer = new Node_Renderer
 
   private def handle_changed(changed_nodes: Set[Document.Node.Name])
   {
     Swing_Thread.now {
       // FIXME correlation to changed_nodes!?

 
       if (nodes_status != nodes_status1) {
         nodes_status = nodes_status1
         status.listData =
           Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
-            .map(_.node)
       }
     }
   }