src/Tools/jEdit/src/session_dockable.scala
changeset 44609 6ec4a5eb2fc0
parent 44335 156be0e43336
child 44613 a3255c85327b
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 17:22:49 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 17:36:10 2011 +0200
     1.3 @@ -10,11 +10,13 @@
     1.4  import isabelle._
     1.5  
     1.6  import scala.actors.Actor._
     1.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
     1.8 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
     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
    1.14 +import javax.swing.JList
    1.15  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.16  
    1.17  import org.gjt.sp.jedit.View
    1.18 @@ -27,11 +29,16 @@
    1.19    private val readme = new HTML_Panel("SansSerif", 14)
    1.20    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    1.21  
    1.22 +  val status = new ListView(Nil: List[String])
    1.23 +  status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
    1.24 +  status.selection.intervalMode = ListView.IntervalMode.Single
    1.25 +
    1.26    private val syslog = new TextArea(Isabelle.session.syslog())
    1.27  
    1.28    private val tabs = new TabbedPane {
    1.29      pages += new TabbedPane.Page("README", Component.wrap(readme))
    1.30 -    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
    1.31 +    pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
    1.32 +    pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
    1.33  
    1.34      selection.index =
    1.35      {
    1.36 @@ -64,6 +71,22 @@
    1.37    add(controls.peer, BorderLayout.NORTH)
    1.38  
    1.39  
    1.40 +  /* component state -- owned by Swing thread */
    1.41 +
    1.42 +  private var nodes: Set[String] = Set.empty
    1.43 +
    1.44 +  private def handle_changed(changed_nodes: Set[String])
    1.45 +  {
    1.46 +    Swing_Thread.now {
    1.47 +      val nodes1 = nodes ++ changed_nodes
    1.48 +      if (nodes1 != nodes) {
    1.49 +        nodes = nodes1
    1.50 +        status.listData = Library.sort_strings(nodes.toList)
    1.51 +      }
    1.52 +    }
    1.53 +  }
    1.54 +
    1.55 +
    1.56    /* main actor */
    1.57  
    1.58    private val main_actor = actor {
    1.59 @@ -83,6 +106,8 @@
    1.60          case phase: Session.Phase =>
    1.61            Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
    1.62  
    1.63 +        case changed: Session.Commands_Changed => handle_changed(changed.nodes)
    1.64 +
    1.65          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
    1.66        }
    1.67      }
    1.68 @@ -91,10 +116,12 @@
    1.69    override def init() {
    1.70      Isabelle.session.raw_messages += main_actor
    1.71      Isabelle.session.phase_changed += main_actor
    1.72 +    Isabelle.session.commands_changed += main_actor
    1.73    }
    1.74  
    1.75    override def exit() {
    1.76      Isabelle.session.raw_messages -= main_actor
    1.77      Isabelle.session.phase_changed -= main_actor
    1.78 +    Isabelle.session.commands_changed -= main_actor
    1.79    }
    1.80  }