global event buses for changes concerning commands and document edits

--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Thu Aug 27 12:12:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Thu Aug 27 16:41:33 2009 +0200
@@ -15,6 +15,7 @@
 import scala.collection.mutable
 
 import isabelle.prover.{Prover, Command}
+import isabelle.proofdocument.ProofDocument
 import isabelle.Isabelle_System
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
@@ -95,11 +96,14 @@
     font_changed.event(font)
   }
 
+  /* event buses */
+
+  val state_update = new EventBus[Command]
+  val command_change = new EventBus[Command]
+  val document_change = new EventBus[ProofDocument]
 
   /* selected state */
 
-  val state_update = new EventBus[Command]
-
   private var _selected_state: Command = null
   def selected_state = _selected_state
   def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Aug 27 12:12:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Aug 27 16:41:33 2009 +0200
@@ -318,6 +318,7 @@
           edits = List(Insert(0, buffer.getText(0, buffer.getLength)))
           commit
         case c: Command =>
+          actor{Isabelle.plugin.command_change.event(c)}
           if(current_document().commands.contains(c))
           Swing_Thread.later {
             // repaint if buffer is active
@@ -327,6 +328,8 @@
               phase_overview.repaint()
             }
           }
+        case d: ProofDocument =>
+          actor{Isabelle.plugin.document_change.event(d)}
         case x => System.err.println("warning: change_receiver ignored " + x)
       }
     }

--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 12:12:11 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 16:41:33 2009 +0200
@@ -147,6 +147,7 @@
                       val state = new Command_State(cmd)
                       states(state_id) = state
                       doc.states += (cmd -> state)
+                      cmd.changed()
                     }
 
                   }
@@ -179,6 +180,7 @@
             val (doc, structure_change) = old.text_changed(change)
             document_versions ::= doc
             edit_document(old, doc, structure_change)
+            change_receiver ! doc
         }
         case x => System.err.println("warning: ignored " + x)
       }