1.1 --- a/src/Pure/library.scala	Wed Aug 31 17:22:49 2011 +0200
     1.2 +++ b/src/Pure/library.scala	Wed Aug 31 17:36:10 2011 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  import scala.swing.ComboBox
     1.5  import scala.swing.event.SelectionChanged
     1.6  import scala.collection.mutable
     1.7 +import scala.util.Sorting
     1.8  
     1.9  
    1.10  object Library
    1.11 @@ -61,6 +62,13 @@
    1.12  
    1.13    def split_lines(str: String): List[String] = space_explode('\n', str)
    1.14  
    1.15 +  def sort_strings(args: Seq[String]): List[String] =
    1.16 +  {
    1.17 +    val a = args.toArray
    1.18 +    Sorting.quickSort(a)
    1.19 +    a.toList
    1.20 +  }
    1.21 +
    1.22  
    1.23    /* iterate over chunks (cf. space_explode) */
    1.24  

     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 31 17:22:49 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 31 17:36:10 2011 +0200
     2.3 @@ -15,7 +15,6 @@
     2.4  
     2.5  import scala.collection.mutable
     2.6  import scala.swing.{ComboBox, ListView, ScrollPane}
     2.7 -import scala.util.Sorting
     2.8  
     2.9  import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
    2.10    Buffer, EditPane, ServiceManager, View}
    2.11 @@ -365,12 +364,11 @@
    2.12        val thys =
    2.13          for (buffer <- buffers; model <- Isabelle.document_model(buffer))
    2.14            yield (model.master_dir, model.thy_name)
    2.15 -      val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
    2.16 +      val files = thy_info.dependencies(thys).toList.map(_._1).filterNot(loaded_buffer _)
    2.17  
    2.18        if (!files.isEmpty) {
    2.19 -        val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
    2.20 -        val files_list = new ListView(files_sorted)
    2.21 -        for (i <- 0 until files_sorted.length)
    2.22 +        val files_list = new ListView(Library.sort_strings(files))
    2.23 +        for (i <- 0 until files.length)
    2.24            files_list.selection.indices += i
    2.25  
    2.26          val answer =

     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 17:22:49 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Aug 31 17:36:10 2011 +0200
     3.3 @@ -10,11 +10,13 @@
     3.4  import isabelle._
     3.5  
     3.6  import scala.actors.Actor._
     3.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
     3.8 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView,
     3.9 +  ScrollPane, TabbedPane, Component, Swing}
    3.10  import scala.swing.event.{ButtonClicked, SelectionChanged}
    3.11  
    3.12  import java.lang.System
    3.13  import java.awt.BorderLayout
    3.14 +import javax.swing.JList
    3.15  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    3.16  
    3.17  import org.gjt.sp.jedit.View
    3.18 @@ -27,11 +29,16 @@
    3.19    private val readme = new HTML_Panel("SansSerif", 14)
    3.20    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    3.21  
    3.22 +  val status = new ListView(Nil: List[String])
    3.23 +  status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
    3.24 +  status.selection.intervalMode = ListView.IntervalMode.Single
    3.25 +
    3.26    private val syslog = new TextArea(Isabelle.session.syslog())
    3.27  
    3.28    private val tabs = new TabbedPane {
    3.29      pages += new TabbedPane.Page("README", Component.wrap(readme))
    3.30 -    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
    3.31 +    pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
    3.32 +    pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
    3.33  
    3.34      selection.index =
    3.35      {
    3.36 @@ -64,6 +71,22 @@
    3.37    add(controls.peer, BorderLayout.NORTH)
    3.38  
    3.39  
    3.40 +  /* component state -- owned by Swing thread */
    3.41 +
    3.42 +  private var nodes: Set[String] = Set.empty
    3.43 +
    3.44 +  private def handle_changed(changed_nodes: Set[String])
    3.45 +  {
    3.46 +    Swing_Thread.now {
    3.47 +      val nodes1 = nodes ++ changed_nodes
    3.48 +      if (nodes1 != nodes) {
    3.49 +        nodes = nodes1
    3.50 +        status.listData = Library.sort_strings(nodes.toList)
    3.51 +      }
    3.52 +    }
    3.53 +  }
    3.54 +
    3.55 +
    3.56    /* main actor */
    3.57  
    3.58    private val main_actor = actor {
    3.59 @@ -83,6 +106,8 @@
    3.60          case phase: Session.Phase =>
    3.61            Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
    3.62  
    3.63 +        case changed: Session.Commands_Changed => handle_changed(changed.nodes)
    3.64 +
    3.65          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
    3.66        }
    3.67      }
    3.68 @@ -91,10 +116,12 @@
    3.69    override def init() {
    3.70      Isabelle.session.raw_messages += main_actor
    3.71      Isabelle.session.phase_changed += main_actor
    3.72 +    Isabelle.session.commands_changed += main_actor
    3.73    }
    3.74  
    3.75    override def exit() {
    3.76      Isabelle.session.raw_messages -= main_actor
    3.77      Isabelle.session.phase_changed -= main_actor
    3.78 +    Isabelle.session.commands_changed -= main_actor
    3.79    }
    3.80  }