--- a/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 10:51:09 2009 +0200
@@ -96,6 +96,15 @@
}
+ /* 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) }
+
+
/* mapping buffer <-> prover */
private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]