--- 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 _ =>
}
}