--- a/src/Tools/jEdit/src/state_dockable.scala Mon Sep 21 17:42:31 2015 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Mon Sep 21 17:59:21 2015 +0200
@@ -111,6 +111,9 @@
case _: Session.Global_Options =>
GUI_Thread.later { handle_resize() }
+ case changed: Session.Commands_Changed =>
+ if (changed.assignment) GUI_Thread.later { maybe_update() }
+
case Session.Caret_Focus =>
GUI_Thread.later { maybe_update() }
}
@@ -118,9 +121,11 @@
override def init()
{
PIDE.session.global_options += main
+ PIDE.session.commands_changed += main
PIDE.session.caret_focus += main
handle_resize()
print_state.activate()
+ maybe_update()
}
override def exit()
@@ -128,6 +133,7 @@
print_state.deactivate()
PIDE.session.caret_focus -= main
PIDE.session.global_options -= main
+ PIDE.session.commands_changed -= main
delay_resize.revoke()
}
}