diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2002-08-09 11:19:07 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-09 11:19:07 +0000 |
commit | a5f35b85555ddaa75a0cd73a76ead9a564b52197 (patch) | |
tree | 75ae0d68feb87b584828a94748705212f34e5fb3 /doc/ProofGeneral.texi | |
parent | a3c93d2541695ae9d8f969ac7e14e69df8586903 (diff) |
Doc comments also under vis control
Diffstat (limited to 'doc/ProofGeneral.texi')
-rw-r--r-- | doc/ProofGeneral.texi | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 109cd79a..5df77e88 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1696,25 +1696,27 @@ you with several escape mechanisms if you want to do this. @section Visibility of completed proofs @cindex Visibility of proofs -Large developments may consist of large files with many proofs. -To help see what has been proved without the detail of the -proof itself, Proof General can hide completed proofs. - -You can toggle the visibility of a proof by using a context sensitive -menu triggered by @b{clicking the right mouse button on a completed -proof}, or the key @kbd{C-c v}, which runs @code{pg-toggle-visibility}. +Large developments may consist of large files with many proofs. To help +see what has been proved without the detail of the proof itself, Proof +General can hide portions of the proof script. Two different kinds of +thing can be hidden: comments and (what Proof General designates as) the +body of proofs. +You can toggle the visibility of a proof script portion by using the +context sensitive menu triggered by @b{clicking the right mouse button +on a completed proof}, or the key @kbd{C-c v}, which runs +@code{pg-toggle-visibility}. You can also select the ``disappearing proofs'' mode from the menu, @lisp Proof-General -> Options -> Disappearing Proofs -@end lisp -This automatically hides each proof as it is completed by the -proof assistant. +@end lisp +This automatically hides each the body of each proof portion +as it is completed by the proof assistant. Finally, two menu commands in the main Proof-General menu, -@emph{Show proofs} and @emph{Hide proofs} apply to all the completed -proofs in the buffer. +@emph{Show all} and @emph{Hide all} apply to all the completed +portions in the buffer. Notice that by design, this feature only applies to completed proofs, @emph{after} they have been processed by the proof assistant. When |