diff -r 318f324d41f5 -r a31730632e13 src/Tools/jEdit/src/state_dockable.scala --- 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("Update") { 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() } }