# HG changeset patch
# User wenzelm
# Date 1314804970 -7200
# Node ID 6ec4a5eb2fc0ac25c7105f680e17924ee0ebb6f9
# Parent  76c2e3ddc183719c0c72de25fdfa45f071c6638f
some support for theory status overview;

diff -r 76c2e3ddc183 -r 6ec4a5eb2fc0 src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Aug 31 17:22:49 2011 +0200
+++ b/src/Pure/library.scala	Wed Aug 31 17:36:10 2011 +0200
@@ -14,6 +14,7 @@
 import scala.swing.ComboBox
 import scala.swing.event.SelectionChanged
 import scala.collection.mutable
+import scala.util.Sorting
 
 
 object Library
@@ -61,6 +62,13 @@
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
+  def sort_strings(args: Seq[String]): List[String] =
+  {
+    val a = args.toArray
+    Sorting.quickSort(a)
+    a.toList
+  }
+
 
   /* iterate over chunks (cf. space_explode) */
 
diff -r 76c2e3ddc183 -r 6ec4a5eb2fc0 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 31 17:22:49 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 31 17:36:10 2011 +0200
@@ -15,7 +15,6 @@
 
 import scala.collection.mutable
 import scala.swing.{ComboBox, ListView, ScrollPane}
-import scala.util.Sorting
 
 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
   Buffer, EditPane, ServiceManager, View}
@@ -365,12 +364,11 @@
       val thys =
         for (buffer <- buffers; model <- Isabelle.document_model(buffer))
           yield (model.master_dir, model.thy_name)
-      val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
+      val files = thy_info.dependencies(thys).toList.map(_._1).filterNot(loaded_buffer _)
 
       if (!files.isEmpty) {
-        val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
-        val files_list = new ListView(files_sorted)
-        for (i <- 0 until files_sorted.length)
+        val files_list = new ListView(Library.sort_strings(files))
+        for (i <- 0 until files.length)
           files_list.selection.indices += i
 
         val answer =
diff -r 76c2e3ddc183 -r 6ec4a5eb2fc0 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
   }
 }