# HG changeset patch
# User wenzelm
# Date 1442844950 -7200
# Node ID 8a5d5ca5d8bc963fd5737afc0dfa6f2e320ec092
# Parent  a3a05d73485800897eb3a7a96e611ae4d7174fc3
added action "isabelle-update-state";
tuned signature;

diff -r a3a05d734858 -r 8a5d5ca5d8bc src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Mon Sep 21 15:55:29 2015 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Mon Sep 21 16:15:50 2015 +0200
@@ -32,6 +32,11 @@
 	    isabelle.jedit.Isabelle.toggle_node_required(view);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle-update-state">
+	  <CODE>
+	    isabelle.jedit.Isabelle.update_state(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.reset-font-size">
 	  <CODE>
 	    isabelle.jedit.Isabelle.reset_font_size();
diff -r a3a05d734858 -r 8a5d5ca5d8bc src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Sep 21 15:55:29 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Sep 21 16:15:50 2015 +0200
@@ -205,6 +205,12 @@
   }
 
 
+  /* update state */
+
+  def update_state(view: View): Unit =
+    state_dockable(view).foreach(_.update())
+
+
   /* ML statistics */
 
   class ML_Stats extends
diff -r a3a05d734858 -r 8a5d5ca5d8bc src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Mon Sep 21 15:55:29 2015 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Sep 21 16:15:50 2015 +0200
@@ -55,41 +55,41 @@
   }
 
 
-  /* caret update */
+  /* update */
 
   private var do_update = true
 
-  private def caret_update()
+  private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() }
+
+  def 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 =>
-      }
+    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") {
+  private val auto_update_button = new CheckBox("Auto update") {
     tooltip = "Indicate automatic update following cursor movement"
-    reactions += { case ButtonClicked(_) => do_update = this.selected; caret_update() }
+    reactions += { case ButtonClicked(_) => do_update = this.selected; maybe_update() }
     selected = do_update
   }
 
-  private val update = new Button("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) }
   }
 
-  private val locate = new Button("Locate") {
+  private val locate_button = new Button("Locate") {
     tooltip = "Locate printed command within source text"
     reactions += { case ButtonClicked(_) => print_state.locate_query() }
   }
@@ -97,11 +97,11 @@
   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
   private val controls =
-    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, locate,
+    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.requestFocus }
+  override def focusOnDefaultComponent { update_button.requestFocus }
 
 
   /* main */
@@ -112,7 +112,7 @@
         GUI_Thread.later { handle_resize() }
 
       case Session.Caret_Focus =>
-        GUI_Thread.later { caret_update() }
+        GUI_Thread.later { maybe_update() }
     }
 
   override def init()