src/Tools/jEdit/src/session_dockable.scala

--- a/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 17:22:49 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 17:36:10 2011 +0200
@@ -10,11 +10,13 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
+  ScrollPane, TabbedPane, Component, Swing}
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 import java.lang.System
 import java.awt.BorderLayout
+import javax.swing.JList
 import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
 import org.gjt.sp.jedit.View
@@ -27,11 +29,16 @@
   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])
+  status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
+  status.selection.intervalMode = ListView.IntervalMode.Single
+
   private val syslog = new TextArea(Isabelle.session.syslog())
 
   private val tabs = new TabbedPane {
     pages += new TabbedPane.Page("README", Component.wrap(readme))
-    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
+    pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
+    pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
 
     selection.index =
     {
@@ -64,6 +71,22 @@
   add(controls.peer, BorderLayout.NORTH)
 
 
+  /* component state -- owned by Swing thread */
+
+  private var nodes: Set[String] = Set.empty
+
+  private def handle_changed(changed_nodes: Set[String])
+  {
+    Swing_Thread.now {
+      val nodes1 = nodes ++ changed_nodes
+      if (nodes1 != nodes) {
+        nodes = nodes1
+        status.listData = Library.sort_strings(nodes.toList)
+      }
+    }
+  }
+
+
   /* main actor */
 
   private val main_actor = actor {
@@ -83,6 +106,8 @@
         case phase: Session.Phase =>
           Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
 
+        case changed: Session.Commands_Changed => handle_changed(changed.nodes)
+
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
       }
     }
@@ -91,10 +116,12 @@
   override def init() {
     Isabelle.session.raw_messages += main_actor
     Isabelle.session.phase_changed += main_actor
+    Isabelle.session.commands_changed += main_actor
   }
 
   override def exit() {
     Isabelle.session.raw_messages -= main_actor
     Isabelle.session.phase_changed -= main_actor
+    Isabelle.session.commands_changed -= main_actor
   }
 }