diff options
| author | David Aspinall | 1999-10-20 16:28:03 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-10-20 16:28:03 +0000 |
| commit | 1ae048201b61b6f32f7c3b11af0525e3d5a35174 (patch) | |
| tree | f516700f74bd62c69a5c301b7a9a32bc791c61c3 /doc | |
| parent | 1c4ae07132770402e07d6c78aacee36833b3bd8b (diff) | |
Fixed crossrefs.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 14 |
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 |
