aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorDavid Aspinall1999-10-20 16:28:03 +0000
committerDavid Aspinall1999-10-20 16:28:03 +0000
commit1ae048201b61b6f32f7c3b11af0525e3d5a35174 (patch)
treef516700f74bd62c69a5c301b7a9a32bc791c61c3 /doc
parent1c4ae07132770402e07d6c78aacee36833b3bd8b (diff)
Fixed crossrefs.
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi14
1 files changed, 5 insertions, 9 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 51847029..61b0984b 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -904,7 +904,7 @@ proofs.
@itemize @bullet
@item The @dfn{proof shell buffer} is an Emacs shell buffer
used to run your proof assistant. Usually it is hidden from view
- (but see @ref{Working directly with the proof shell}).
+ (but see @ref{Escaping script management}).
Communication with the proof shell takes place via two or three
intermediate buffers.
@item A @dfn{script buffer}, as we have explained, is a buffer for editing a
@@ -1236,11 +1236,7 @@ returns false, then an error message is given.
As if the last two commands weren't risky enough, there's also a command
which explicitly adjusts the end of the locked region, to be used in
-extreme circumstances only. @xref{Working directly with the proof
-shell}.
-
-@c Perhaps, don't explain C-c C-z here. Instead refer to @pxref{Working
-@c directly with the proof shell}
+extreme circumstances only. @xref{Escaping script management}.
There are a few commands for stopping, starting, and restarting the
proof assistant process which have menu entries but no key bindings.
@@ -1311,7 +1307,7 @@ you with several escape mechanisms if you want to do this.
* View of processed files ::
* Retracting across files::
* Asserting across files::
-* Escaping script managment::
+* Escaping script management::
@end menu
@node Switching between proof scripts
@@ -1413,8 +1409,8 @@ unmodified buffers. This is particularly useful as assertion may cause
the proof assistant to automatically process other files.
-@node Escaping script managment
-@section Escaping script managment
+@node Escaping script management
+@section Escaping script management
@cindex Shell
Occasionally you may want to review the dialogue of the entire session