# HG changeset patch
# User wenzelm
# Date 1260305292 -3600
# Node ID 8dd19c5f8c56ffae2df02c4f4254696783bfe639
# Parent  4f9bcd4b5bd1ab12a23909ad9f6df398936f9395
added properties_changed event bus;

diff -r 4f9bcd4b5bd1 -r 8dd19c5f8c56 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 21:01:16 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 21:48:12 2009 +0100
@@ -87,6 +87,7 @@
   /* event buses */
 
   val state_update = new Event_Bus[Command]
+  val properties_changed = new Event_Bus[Unit]
 
 
   /* selected state */
@@ -121,12 +122,12 @@
 
   /* main plugin plumbing */
 
-  override def handleMessage(msg: EBMessage)
+  override def handleMessage(message: EBMessage)
   {
-    msg match {
-      case epu: EditPaneUpdate =>
-        val buffer = epu.getEditPane.getBuffer
-        epu.getWhat match {
+    message match {
+      case msg: EditPaneUpdate =>
+        val buffer = msg.getEditPane.getBuffer
+        msg.getWhat match {
           case EditPaneUpdate.BUFFER_CHANGED =>
             (mapping get buffer) map (_.theory_view.activate)
           case EditPaneUpdate.BUFFER_CHANGING =>
@@ -134,6 +135,7 @@
               (mapping get buffer) map (_.theory_view.deactivate)
           case _ =>
         }
+      case msg: PropertiesChanged => properties_changed.event(())
       case _ =>
     }
   }