diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-10-01 16:16:53 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-10-01 16:16:53 +0000 |
| commit | 58472ae80b692c593306003123b19780c4d11838 (patch) | |
| tree | 38aff9c0ca5c4d89369926262ecdd9307ff1298f /doc/PG-adapting.texi | |
| parent | 27116fe22a0ef9b535c23a3163e8dab9d9e3b65e (diff) | |
Document query identifier
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 4 |
1 files changed, 3 insertions, 1 deletions
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 |