# HG changeset patch # User wenzelm # Date 1442843729 -7200 # Node ID a3a05d73485800897eb3a7a96e611ae4d7174fc3 # Parent 7a421e7ef97c3220b06309e2de7ba31cdda28f43 support for auto update via caret focus; diff -r 7a421e7ef97c -r a3a05d734858 src/Pure/PIDE/query_operation.scala --- a/src/Pure/PIDE/query_operation.scala Mon Sep 21 15:07:23 2015 +0200 +++ b/src/Pure/PIDE/query_operation.scala Mon Sep 21 15:55:29 2015 +0200 @@ -38,6 +38,8 @@ @volatile private var current_status = Query_Operation.Status.FINISHED @volatile private var current_exec_id = Document_ID.none + def get_location: Option[Command] = current_location + private def reset_state() { current_location = None diff -r 7a421e7ef97c -r a3a05d734858 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Mon Sep 21 15:07:23 2015 +0200 +++ b/src/Tools/jEdit/src/state_dockable.scala Mon Sep 21 15:55:29 2015 +0200 @@ -55,8 +55,35 @@ } + /* caret update */ + + private var do_update = true + + private def caret_update() + { + GUI_Thread.require {} + + if (do_update) { + PIDE.document_model(view.getBuffer).map(_.snapshot()) match { + 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 None => + } + } + } + + /* controls */ + private val auto_update = new CheckBox("Auto update") { + tooltip = "Indicate automatic update following cursor movement" + reactions += { case ButtonClicked(_) => do_update = this.selected; caret_update() } + selected = do_update + } + private val update = new Button("Update") { tooltip = "Update display according to the command at cursor position" reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) } @@ -70,7 +97,7 @@ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)(update, locate, + new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, locate, pretty_text_area.search_label, pretty_text_area.search_field, zoom) add(controls.peer, BorderLayout.NORTH) @@ -83,11 +110,15 @@ Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => GUI_Thread.later { handle_resize() } + + case Session.Caret_Focus => + GUI_Thread.later { caret_update() } } override def init() { PIDE.session.global_options += main + PIDE.session.caret_focus += main handle_resize() print_state.activate() } @@ -95,6 +126,7 @@ override def exit() { print_state.deactivate() + PIDE.session.caret_focus -= main PIDE.session.global_options -= main delay_resize.revoke() }