1.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 12 13:43:55 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 12 13:49:08 2010 +0200
     1.3 @@ -13,9 +13,6 @@
     1.4  import scala.collection.mutable
     1.5  
     1.6  
     1.7 -case class Command_Set(set: Set[Command])
     1.8 -
     1.9 -
    1.10  object Command
    1.11  {
    1.12    object Status extends Enumeration

     2.1 --- a/src/Pure/System/session.scala	Thu Aug 12 13:43:55 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Thu Aug 12 13:49:08 2010 +0200
     2.3 @@ -19,6 +19,8 @@
     2.4  
     2.5    case object Global_Settings
     2.6    case object Perspective
     2.7 +  case class Commands_Changed(set: Set[Command])
     2.8 +
     2.9  
    2.10  
    2.11    /* managed entities */
    2.12 @@ -52,7 +54,7 @@
    2.13    val global_settings = new Event_Bus[Session.Global_Settings.type]
    2.14    val raw_results = new Event_Bus[Isabelle_Process.Result]
    2.15    val raw_output = new Event_Bus[Isabelle_Process.Result]
    2.16 -  val commands_changed = new Event_Bus[Command_Set]
    2.17 +  val commands_changed = new Event_Bus[Session.Commands_Changed]
    2.18    val perspective = new Event_Bus[Session.Perspective.type]
    2.19  
    2.20  
    2.21 @@ -282,7 +284,7 @@
    2.22  
    2.23      def flush()
    2.24      {
    2.25 -      if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
    2.26 +      if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
    2.27        changed = Set()
    2.28        flush_time = None
    2.29      }

     3.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 12 13:43:55 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 12 13:49:08 2010 +0200
     3.3 @@ -103,7 +103,7 @@
     3.4    private val commands_changed_actor = actor {
     3.5      loop {
     3.6        react {
     3.7 -        case Command_Set(changed) =>
     3.8 +        case Session.Commands_Changed(changed) =>
     3.9            Swing_Thread.now {
    3.10              // FIXME cover doc states as well!!?
    3.11              val snapshot = model.snapshot()

     4.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 12 13:43:55 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 12 13:49:08 2010 +0200
     4.3 @@ -87,7 +87,7 @@
     4.4      loop {
     4.5        react {
     4.6          case Session.Global_Settings => handle_resize()
     4.7 -        case Command_Set(changed) => handle_update(Some(changed))
     4.8 +        case Session.Commands_Changed(changed) => handle_update(Some(changed))
     4.9          case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
    4.10          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    4.11        }