src/Tools/jEdit/src/session_dockable.scala
changeset 44957 098dd95349e7
parent 44867 79d3d74e7cbb
child 44958 86e4916825ee
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 19:55:32 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 21:28:52 2011 +0200
     1.3 @@ -10,13 +10,13 @@
     1.4  import isabelle._
     1.5  
     1.6  import scala.actors.Actor._
     1.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
     1.8 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
     1.9    ScrollPane, TabbedPane, Component, Swing}
    1.10  import scala.swing.event.{ButtonClicked, SelectionChanged}
    1.11  
    1.12  import java.lang.System
    1.13 -import java.awt.{BorderLayout, Graphics}
    1.14 -import javax.swing.{JList, DefaultListCellRenderer}
    1.15 +import java.awt.{BorderLayout, Graphics2D}
    1.16 +import javax.swing.{JList, DefaultListCellRenderer, UIManager}
    1.17  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.18  
    1.19  import org.gjt.sp.jedit.{View, jEdit}
    1.20 @@ -29,7 +29,7 @@
    1.21    private val readme = new HTML_Panel("SansSerif", 14)
    1.22    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    1.23  
    1.24 -  val status = new ListView(Nil: List[String])
    1.25 +  val status = new ListView(Nil: List[Document.Node.Name])
    1.26    status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
    1.27    status.selection.intervalMode = ListView.IntervalMode.Single
    1.28  
    1.29 @@ -86,11 +86,15 @@
    1.30  
    1.31    private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
    1.32  
    1.33 -  val node_renderer = new DefaultListCellRenderer
    1.34 +  private class Node_Renderer_Component extends Label
    1.35    {
    1.36 -    override def paintComponent(gfx: Graphics)
    1.37 +    xAlignment = Alignment.Leading
    1.38 +    border = UIManager.getBorder("List.cellNoFocusBorder")
    1.39 +
    1.40 +    var node_name = Document.Node.Name.empty
    1.41 +    override def paintComponent(gfx: Graphics2D)
    1.42      {
    1.43 -      nodes_status.get(Document.Node.Name(getText, "", "")) match {
    1.44 +      nodes_status.get(node_name) match {
    1.45          case Some(st) if st.total > 0 =>
    1.46            val w = getWidth
    1.47            val h = getHeight
    1.48 @@ -112,7 +116,19 @@
    1.49      }
    1.50    }
    1.51  
    1.52 -  status.peer.setCellRenderer(node_renderer)
    1.53 +  private class Node_Renderer extends
    1.54 +    ListView.AbstractRenderer[Document.Node.Name, Node_Renderer_Component](
    1.55 +      new Node_Renderer_Component)
    1.56 +  {
    1.57 +    def configure(list: ListView[_], isSelected: Boolean, focused: Boolean,
    1.58 +      name: Document.Node.Name, index: Int)
    1.59 +    {
    1.60 +      component.opaque = false
    1.61 +      component.node_name = name
    1.62 +      component.text = name.theory
    1.63 +    }
    1.64 +  }
    1.65 +  status.renderer = new Node_Renderer
    1.66  
    1.67    private def handle_changed(changed_nodes: Set[Document.Node.Name])
    1.68    {
    1.69 @@ -132,7 +148,6 @@
    1.70          nodes_status = nodes_status1
    1.71          status.listData =
    1.72            Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
    1.73 -            .map(_.node)
    1.74        }
    1.75      }
    1.76    }