# HG changeset patch
# User wenzelm
# Date 1316287732 -7200
# Node ID 098dd95349e763ae982aef2aebb01a1894590900
# Parent  01a1b3b3341f4d8fb5dc60f069213abd18c5db06
more elaborate Node_Renderer, which paints node_name.theory only;

diff -r 01a1b3b3341f -r 098dd95349e7 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Sep 17 19:55:32 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Sep 17 21:28:52 2011 +0200
@@ -39,6 +39,10 @@
 
   object Node
   {
+    object Name
+    {
+      val empty = Name("", "", "")
+    }
     sealed case class Name(node: String, dir: String, theory: String)
     {
       override def hashCode: Int = node.hashCode
diff -r 01a1b3b3341f -r 098dd95349e7 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 19:55:32 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 21:28:52 2011 +0200
@@ -10,13 +10,13 @@
 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}
@@ -29,7 +29,7 @@
   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
 
@@ -86,11 +86,15 @@
 
   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
@@ -112,7 +116,19 @@
     }
   }
 
-  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])
   {
@@ -132,7 +148,6 @@
         nodes_status = nodes_status1
         status.listData =
           Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
-            .map(_.node)
       }
     }
   }