# HG changeset patch # User wenzelm # Date 1449497885 -3600 # Node ID fa8d1cdf6518af8e0e0b3d4a6459b40cbb6459b1 # Parent f3789d5b96caef00b3247781a5e66d336be0836b tuned signature; diff -r f3789d5b96ca -r fa8d1cdf6518 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Mon Dec 07 15:16:28 2015 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Mon Dec 07 15:18:05 2015 +0100 @@ -57,9 +57,8 @@ /* update */ - private var do_update = true - - private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() } + def update_request(): Unit = + GUI_Thread.require { print_state.apply_query(Nil) } def update() { @@ -69,24 +68,32 @@ case Some(snapshot) => (PIDE.editor.current_command(view, snapshot), print_state.get_location) match { case (Some(command1), Some(command2)) if command1.id == command2.id => - case _ => print_state.apply_query(Nil) + case _ => update_request() } case None => } } + /* auto update */ + + private var auto_update_enabled = true + + private def auto_update(): Unit = + GUI_Thread.require { if (auto_update_enabled) update() } + + /* 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 + reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() } + selected = auto_update_enabled } 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) } + reactions += { case ButtonClicked(_) => update_request() } } private val locate_button = new Button("Locate") { @@ -112,10 +119,10 @@ GUI_Thread.later { handle_resize() } case changed: Session.Commands_Changed => - if (changed.assignment) GUI_Thread.later { maybe_update() } + if (changed.assignment) GUI_Thread.later { auto_update() } case Session.Caret_Focus => - GUI_Thread.later { maybe_update() } + GUI_Thread.later { auto_update() } } override def init() @@ -125,7 +132,7 @@ PIDE.session.caret_focus += main handle_resize() print_state.activate() - maybe_update() + auto_update() } override def exit()