From 6c27574f147610c3062ae1480c9a595804694c41 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 8 Nov 1999 18:33:29 +0000
Subject: Added a section on debugging, mentioned proof-show-debug-messages.

---
 doc/ProofGeneral.texi | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 645259a2..d5dc21b6 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3393,6 +3393,7 @@ important files, kept in the @file{generic/} subdirectory.
 * Global variables::            
 * Proof script mode::           
 * Proof shell mode::            
+* Debugging::
 @end menu
 
 
@@ -3921,7 +3922,7 @@ object files, used by Lego and Coq).
 @c
 @c INPUT
 @c
-@subsubsection Input
+@subsection Input to the shell
 
 Input to the proof shell via the queue region is managed by the
 functions @code{proof-start-queue} and @code{proof-shell-exec-loop}.
@@ -3985,7 +3986,7 @@ particularly in @code{proof-start-queue} and @code{proof-shell-exec-loop}.
 @c
 @c OUTPUT
 @c
-@subsubsection Output
+@subsection Output from the shell
 
 Two main functions deal with output, @code{proof-shell-process-output}
 and @code{proof-shell-process-urgent-message}.  In effect we consider
@@ -4095,7 +4096,21 @@ output.
 
 
 
+@c
+@c SECTION: Debugging
+@c
+@node Debugging
+@section Debugging
+@cindex debugging
+
+To debug Proof General, it may be helpful to set the
+configuration variable @code{proof-show-debug-messages}.
+
+@c TEXI DOCSTRING MAGIC: proof-show-debug-messages
 
+For more information about debugging Emacs lisp, consult the Emacs Lisp
+Reference Manual.  I recommend using the source-level debugger
+@code{edebug}.
 
 
 
-- 
cgit v1.2.3