--- a/src/Tools/jEdit/src/jedit/Plugin.scala Mon Sep 07 21:09:26 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Mon Sep 07 22:17:51 2009 +0200
@@ -87,7 +87,7 @@
/* Isabelle font */
var font: Font = null
- val font_changed = new EventBus[Font]
+ val font_changed = new Event_Bus[Font]
def set_font(size: Int)
{
@@ -100,9 +100,9 @@
/* event buses */
- val state_update = new EventBus[Command]
- val command_change = new EventBus[Command]
- val document_change = new EventBus[ProofDocument]
+ val state_update = new Event_Bus[Command]
+ val command_change = new Event_Bus[Command]
+ val document_change = new Event_Bus[ProofDocument]
/* selected state */