# HG changeset patch
# User wenzelm
# Date 1281613748 -7200
# Node ID 53224a4d2f0e5f1d33e77097555de5fcf3deca3f
# Parent  96b22dfeb56a20cee664051db1bb2ddd38d7bdb1
specific Session.Commands_Changed;

diff -r 96b22dfeb56a -r 53224a4d2f0e src/Pure/PIDE/command.scala
--- 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
diff -r 96b22dfeb56a -r 53224a4d2f0e src/Pure/System/session.scala
--- 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
     }
diff -r 96b22dfeb56a -r 53224a4d2f0e src/Tools/jEdit/src/jedit/document_view.scala
--- 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()
diff -r 96b22dfeb56a -r 53224a4d2f0e src/Tools/jEdit/src/jedit/output_dockable.scala
--- 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)
       }