From 58472ae80b692c593306003123b19780c4d11838 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 1 Oct 2010 16:16:53 +0000 Subject: Document query identifier --- doc/PG-adapting.texi | 4 +++- doc/ProofGeneral.texi | 16 ++++++++++++---- 2 files changed, 15 insertions(+), 5 deletions(-) (limited to 'doc') 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 -- cgit v1.2.3