diff options
| -rw-r--r-- | doc/PG-adapting.texi | 31 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 2 |
2 files changed, 15 insertions, 18 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index fd6edd77..4eced60c 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1047,7 +1047,7 @@ Function to return list of commands to forget to before its argument span.@* This setting is used to for retraction (undoing) in proof scripts. It should undo the effect of all settings between its target span -up to (@code{proof-locked-end}). This may involve forgetting a number +up to (@code{proof-unprocessed-begin}). This may involve forgetting a number of definitions, declarations, or whatever. If return value is nil, it means there is nothing to do. @@ -3213,9 +3213,8 @@ interaction with the process. @c TEXI DOCSTRING MAGIC: proof-shell-busy @defvar proof-shell-busy A lock indicating that the proof shell is processing.@* -This is either a queue mode indication ('advancing,'retracting) or -t for a non-scripting command. -When this is non-nil, @samp{@code{proof-shell-ready-prover}} will give an error. +When this is non-nil, @code{proof-shell-ready-prover} will give +an error. @end defvar @c TEXI DOCSTRING MAGIC: proof-marker @@ -3240,7 +3239,7 @@ commands (out of script). They may include If flags are non-empty, other interactive cues will be surpressed. (E.g., printing help messages). -See the functions @samp{@code{proof-extend-queue}} and @samp{@code{proof-shell-exec-loop}}. +See the functions @samp{@code{proof-start-queue}} and @samp{@code{proof-shell-exec-loop}}. @end defvar @c TEXI DOCSTRING MAGIC: pg-subterm-anns-use-stack @@ -3328,21 +3327,19 @@ Input to the proof shell via the queue region is managed by the functions @code{proof-extend-queue} and @code{proof-shell-exec-loop}. @c TEXI DOCSTRING MAGIC: proof-extend-queue -@defun proof-extend-queue start end queueitems queuemode -Extend the command queue with @var{queueitems}, in mode @var{queuemode}.@* -If @var{start} is non-nil, @var{start} and @var{end} are buffer positions in the -active scripting buffer for the queue region. -If the queue is non-empty, @var{queuemode} ought to match the current -setting (this is not checked). +@defun proof-extend-queue end queueitems +Extend the current queue with @var{queueitems}, queue end @var{end}.@* +To make sense, the commands should correspond to processing actions +for processing a region from (buffer-queue-or-locked-end) to @var{end}. +The queue mode is set to @code{'advancing} @end defun @c TEXI DOCSTRING MAGIC: proof-extend-queue -@defun proof-extend-queue start end queueitems queuemode -Extend the command queue with @var{queueitems}, in mode @var{queuemode}.@* -If @var{start} is non-nil, @var{start} and @var{end} are buffer positions in the -active scripting buffer for the queue region. -If the queue is non-empty, @var{queuemode} ought to match the current -setting (this is not checked). +@defun proof-extend-queue end queueitems +Extend the current queue with @var{queueitems}, queue end @var{end}.@* +To make sense, the commands should correspond to processing actions +for processing a region from (buffer-queue-or-locked-end) to @var{end}. +The queue mode is set to @code{'advancing} @end defun @vindex proof-action-list @c TEXI DOCSTRING MAGIC: proof-shell-exec-loop diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index e477a8a0..0442d084 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4139,7 +4139,7 @@ The default value is @code{nil}. @end defopt @c TEXI DOCSTRING MAGIC: isabelle-choose-logic @deffn Command isabelle-choose-logic logic -Adjust @code{isabelle-prog-name} and @code{proof-prog-name} for running @var{logic}. +Adjust isabelle-prog-name and @code{proof-prog-name} for running @var{logic}. @end deffn @node Isabelle commands @section Isabelle commands |