# 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()
   }