From f652439d60110cf171b16f2348edbe988199a92c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 19 Jun 2002 00:30:13 +0000
Subject: Add doc of proof-shell-last-prompt.

---
 doc/PG-adapting.texi | 14 +++++++++++---
 1 file 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.
-- 
cgit v1.2.3