more elaborate Node_Renderer, which paints node_name.theory only;
authorwenzelm
Sat Sep 17 21:28:52 2011 +0200 (2011-09-17 ago)
changeset 44957098dd95349e7
parent 44956 01a1b3b3341f
child 44958 86e4916825ee
more elaborate Node_Renderer, which paints node_name.theory only;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Sep 17 19:55:32 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Sep 17 21:28:52 2011 +0200
     1.3 @@ -39,6 +39,10 @@
     1.4  
     1.5    object Node
     1.6    {
     1.7 +    object Name
     1.8 +    {
     1.9 +      val empty = Name("", "", "")
    1.10 +    }
    1.11      sealed case class Name(node: String, dir: String, theory: String)
    1.12      {
    1.13        override def hashCode: Int = node.hashCode
     2.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 19:55:32 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 21:28:52 2011 +0200
     2.3 @@ -10,13 +10,13 @@
     2.4  import isabelle._
     2.5  
     2.6  import scala.actors.Actor._
     2.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
     2.8 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
     2.9    ScrollPane, TabbedPane, Component, Swing}
    2.10  import scala.swing.event.{ButtonClicked, SelectionChanged}
    2.11  
    2.12  import java.lang.System
    2.13 -import java.awt.{BorderLayout, Graphics}
    2.14 -import javax.swing.{JList, DefaultListCellRenderer}
    2.15 +import java.awt.{BorderLayout, Graphics2D}
    2.16 +import javax.swing.{JList, DefaultListCellRenderer, UIManager}
    2.17  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    2.18  
    2.19  import org.gjt.sp.jedit.{View, jEdit}
    2.20 @@ -29,7 +29,7 @@
    2.21    private val readme = new HTML_Panel("SansSerif", 14)
    2.22    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    2.23  
    2.24 -  val status = new ListView(Nil: List[String])
    2.25 +  val status = new ListView(Nil: List[Document.Node.Name])
    2.26    status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
    2.27    status.selection.intervalMode = ListView.IntervalMode.Single
    2.28  
    2.29 @@ -86,11 +86,15 @@
    2.30  
    2.31    private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
    2.32  
    2.33 -  val node_renderer = new DefaultListCellRenderer
    2.34 +  private class Node_Renderer_Component extends Label
    2.35    {
    2.36 -    override def paintComponent(gfx: Graphics)
    2.37 +    xAlignment = Alignment.Leading
    2.38 +    border = UIManager.getBorder("List.cellNoFocusBorder")
    2.39 +
    2.40 +    var node_name = Document.Node.Name.empty
    2.41 +    override def paintComponent(gfx: Graphics2D)
    2.42      {
    2.43 -      nodes_status.get(Document.Node.Name(getText, "", "")) match {
    2.44 +      nodes_status.get(node_name) match {
    2.45          case Some(st) if st.total > 0 =>
    2.46            val w = getWidth
    2.47            val h = getHeight
    2.48 @@ -112,7 +116,19 @@
    2.49      }
    2.50    }
    2.51  
    2.52 -  status.peer.setCellRenderer(node_renderer)
    2.53 +  private class Node_Renderer extends
    2.54 +    ListView.AbstractRenderer[Document.Node.Name, Node_Renderer_Component](
    2.55 +      new Node_Renderer_Component)
    2.56 +  {
    2.57 +    def configure(list: ListView[_], isSelected: Boolean, focused: Boolean,
    2.58 +      name: Document.Node.Name, index: Int)
    2.59 +    {
    2.60 +      component.opaque = false
    2.61 +      component.node_name = name
    2.62 +      component.text = name.theory
    2.63 +    }
    2.64 +  }
    2.65 +  status.renderer = new Node_Renderer
    2.66  
    2.67    private def handle_changed(changed_nodes: Set[Document.Node.Name])
    2.68    {
    2.69 @@ -132,7 +148,6 @@
    2.70          nodes_status = nodes_status1
    2.71          status.listData =
    2.72            Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
    2.73 -            .map(_.node)
    2.74        }
    2.75      }
    2.76    }