diff options
| author | David Aspinall | 2002-06-19 00:30:13 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-06-19 00:30:13 +0000 |
| commit | f652439d60110cf171b16f2348edbe988199a92c (patch) | |
| tree | 2c543336e8847d45370bf83513d75b98df7a427c | |
| parent | 2a217ab5d65ec07598832c0bb04e98ea6c9be886 (diff) | |
Add doc of proof-shell-last-prompt.
| -rw-r--r-- | doc/PG-adapting.texi | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 9750c868..899ce024 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3270,12 +3270,20 @@ last urgent message seen. When output is grabbed from the prover process, it is stored into @code{proof-shell-last-output}, and its type is stored in -@code{proof-shell-last-output-kind}. Output which is deferred -or possibly discarded until the queue is empty is copied into +@code{proof-shell-last-output-kind}. Output which is deferred or +possibly discarded until the queue is empty is copied into @code{proof-shell-delayed-output}, with type -@code{proof-shell-delayed-output-kind}. +@code{proof-shell-delayed-output-kind}. A record of the last prompt +seen from the prover process is also kept, in +@code{proof-shell-last-prompt}. +@c TEXI DOCSTRING MAGIC: proof-shell-last-prompt + +@defvar proof-shell-last-prompt +A record of the last prompt seen from the proof system.@* +This is the string matched by @code{proof-shell-annotated-prompt-regexp}. +@end defvar @c TEXI DOCSTRING MAGIC: proof-shell-last-output @defvar proof-shell-last-output A record of the last string seen from the proof system. |