# HG changeset patch
# User wenzelm
# Date 1442859689 -7200
# Node ID 04c769fe1cb540d0f20f08e811a8240b8168b004
# Parent  566f256f59bbf9d528ffa3388e270c9254605917
clarified isabelle.update-state;

diff -r 566f256f59bb -r 04c769fe1cb5 NEWS
--- a/NEWS	Mon Sep 21 17:59:21 2015 +0200
+++ b/NEWS	Mon Sep 21 20:21:29 2015 +0200
@@ -28,11 +28,11 @@
 asynchronously, leading to much better editor reactivity. Moreover, the
 full document node content is taken into account.
 
-* The State panel manages implicit proof state output, with jEdit action
-"isabelle-update-state" to trigger update according to cursor position.
-Option "editor_output_state" controls implicit proof state output in the
-Output panel: suppressing this may reduce resource requirements of
-prover time and GUI space.
+* The State panel manages explicit proof state output, with jEdit action
+"isabelle.update-state" (shortcut S+ENTER) to trigger update according
+to cursor position. Option "editor_output_state" controls implicit proof
+state output in the Output panel: suppressing this reduces resource
+requirements of prover time and GUI space.
 
 
 *** Isar ***
diff -r 566f256f59bb -r 04c769fe1cb5 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Mon Sep 21 17:59:21 2015 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Mon Sep 21 20:21:29 2015 +0200
@@ -32,7 +32,7 @@
 	    isabelle.jedit.Isabelle.toggle_node_required(view);
 	  </CODE>
 	</ACTION>
-	<ACTION NAME="isabelle-update-state">
+	<ACTION NAME="isabelle.update-state">
 	  <CODE>
 	    isabelle.jedit.Isabelle.update_state(view);
 	  </CODE>
diff -r 566f256f59bb -r 04c769fe1cb5 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Mon Sep 21 17:59:21 2015 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Sep 21 20:21:29 2015 +0200
@@ -232,6 +232,8 @@
 isabelle.toggle-continuous-checking.shortcut=C+e ENTER
 isabelle.toggle-node-required.label=Toggle node required
 isabelle.toggle-node-required.shortcut=C+e SPACE
+isabelle.update-state.label=Update state output
+isabelle.update-state.shortcut=S+ENTER
 lang.usedefaultlocale=false
 largefilemode=full
 line-end.shortcut=END