Document query identifier

3 files changed, 18 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index 341d38a5..eba64ee2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,7 +45,6 @@
     making a keyboard/mouse action.
     See the manual for more details.
 
-
 *** Fast buffer processing option
       Quick Options -> Processing -> Fast Process Buffer
     This affects 'proof-process-buffer' (C-c C-b, toolbar down).
@@ -63,6 +62,9 @@
 *** Proof General -> Options menu extended and rearranged
     - new menu for useful minor modes indicates modes that PG supports
 
+*** New query identifier info button and command (C-c C-i, C-M-mouse1)
+    These are convenience commands for looking up identifiers in the running prover.
+
 *** New user configuration options (also on Proof General -> Options)
     proof-colour-locked       (use background colour for checked text)
     proof-auto-raise-buffers  (set to nil for manual window control)
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index b0aac648..1e30760b 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -2589,7 +2589,8 @@ In case @var{cmd} is (or yields) nil, do nothing.
 if it is set.  It should probably run the hook variables
 @samp{@code{proof-state-change-hook}}.
 
-@var{flags} are put onto the If @var{noerror} is set, surpress usual error action.
+@var{flags} are additional flags to put onto the @samp{@code{proof-action-list}}.
+The flag @code{'invisible} is always added to @var{flags}.
 @end defun
 
 There are several handy macros to help you define functions
@@ -3282,6 +3283,7 @@ which is the queue of things to do.  The display flags are set
 for non-scripting commands or for when scripting should not
 bother the user.  They may include
 @lisp
+  @code{'invisible}             non-script command (@samp{@code{proof-shell-invisible-command}})
   @code{'no-response-display}   do not display messages in @strong{response} buffer
   @code{'no-error-display}      do not display errors/take error action
   @code{'no-goals-display}      do not goals in @strong{goals} buffer
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 32b73f02..19d8b8ac 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1500,6 +1500,8 @@ key-bindings and functions.
 @code{proof-ctxt}
 @item C-c C-h
 @code{proof-help}
+@item C-c C-i
+@code{proof-query-identifier}
 @item C-c C-f
 @code{proof-find-theorems}
 @item C-c C-w
@@ -1545,6 +1547,11 @@ Typically, a list of syntax of commands available.
 Issues a command to the assistant based on @code{proof-info-command}.
 @end deffn
 
+@c TEXI DOCSTRING MAGIC: proof-query-identifier
+@deffn Command proof-query-identifier string
+Query the prover about the identifier @var{string}.@*
+If called interactively, @var{string} defaults to the current word near point.
+@end deffn
 @c TEXI DOCSTRING MAGIC: proof-find-theorems
 @deffn Command proof-find-theorems arg
 Search for items containing given constants.@*
@@ -1657,10 +1664,11 @@ object files, used by Lego and Coq).
 @section Toolbar commands
 
 The toolbar provides a selection of functions for asserting and
-retracting portions of the script, issuing non-scripting commands, and
-inserting "goal" and "save" type commands.  The latter functions are not
-available on keys, but are available from the from the menu, or via
-@kbd{M-x}, as well as the toolbar.
+retracting portions of the script, issuing non-scripting commands to
+inspect the prover's state, and inserting "goal" and "save" type
+commands.  The latter functions are not available on keys, but are
+available from the from the menu, or via @kbd{M-x}, as well as the
+toolbar.
 
 @c TEXI DOCSTRING MAGIC: proof-issue-goal
 @deffn Command proof-issue-goal arg