--- a/src/Pure/PIDE/command.scala Thu Aug 12 13:43:55 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu Aug 12 13:49:08 2010 +0200
@@ -13,9 +13,6 @@
import scala.collection.mutable
-case class Command_Set(set: Set[Command])
-
-
object Command
{
object Status extends Enumeration
--- a/src/Pure/System/session.scala Thu Aug 12 13:43:55 2010 +0200
+++ b/src/Pure/System/session.scala Thu Aug 12 13:49:08 2010 +0200
@@ -19,6 +19,8 @@
case object Global_Settings
case object Perspective
+ case class Commands_Changed(set: Set[Command])
+
/* managed entities */
@@ -52,7 +54,7 @@
val global_settings = new Event_Bus[Session.Global_Settings.type]
val raw_results = new Event_Bus[Isabelle_Process.Result]
val raw_output = new Event_Bus[Isabelle_Process.Result]
- val commands_changed = new Event_Bus[Command_Set]
+ val commands_changed = new Event_Bus[Session.Commands_Changed]
val perspective = new Event_Bus[Session.Perspective.type]
@@ -282,7 +284,7 @@
def flush()
{
- if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
+ if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
changed = Set()
flush_time = None
}
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 12 13:43:55 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 12 13:49:08 2010 +0200
@@ -103,7 +103,7 @@
private val commands_changed_actor = actor {
loop {
react {
- case Command_Set(changed) =>
+ case Session.Commands_Changed(changed) =>
Swing_Thread.now {
// FIXME cover doc states as well!!?
val snapshot = model.snapshot()
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Aug 12 13:43:55 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Aug 12 13:49:08 2010 +0200
@@ -87,7 +87,7 @@
loop {
react {
case Session.Global_Settings => handle_resize()
- case Command_Set(changed) => handle_update(Some(changed))
+ case Session.Commands_Changed(changed) => handle_update(Some(changed))
case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
}