--- a/src/Tools/jEdit/src/state_dockable.scala Sat Nov 21 15:45:09 2015 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Sat Nov 21 16:06:36 2015 +0100
@@ -57,6 +57,10 @@
/* update */
+ private var do_update = true
+
+ private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() }
+
def update()
{
GUI_Thread.require {}
@@ -74,6 +78,12 @@
/* controls */
+ private val auto_update_button = new CheckBox("Auto update") {
+ tooltip = "Indicate automatic update following cursor movement"
+ reactions += { case ButtonClicked(_) => do_update = this.selected; maybe_update() }
+ selected = do_update
+ }
+
private val update_button = new Button("<html><b>Update</b></html>") {
tooltip = "Update display according to the command at cursor position"
reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) }
@@ -87,8 +97,8 @@
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(update_button, locate_button,
- pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update_button, update_button,
+ locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)
add(controls.peer, BorderLayout.NORTH)
override def focusOnDefaultComponent { update_button.requestFocus }
@@ -100,19 +110,30 @@
Session.Consumer[Any](getClass.getName) {
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() }
}
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()
{
print_state.deactivate()
+ PIDE.session.caret_focus -= main
PIDE.session.global_options -= main
+ PIDE.session.commands_changed -= main
delay_resize.revoke()
}
}