| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
mizar-make-reserve-summary
mizar-make-theorem-summary
Make a summary of all type reservations before current point in the article.
Display it in the ‘Occur’ buffer, which uses the ‘occur-mode’.
Previous contents of that buffer are killed first.
Useful for finding out the exact meaning of variables used in
some Mizar theorem or definition.
Make a smmary of the theorems in the the current buffer.The
output will be put into a buffer called "*Theorem-Summary*"; if
that buffer already exists when this command is called, its
contents will be erased.
(The command ‘hs-hide-all’, accessible from the Hide/Show menu,
can be used instead of ‘mizar-make-theorem-summary’ to make a
summary of an article.)
| 3.1 Hide/Show - Hiding proofs |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
hs-mouse-toggle-hiding
Mizar Mode customizes the standard Hide/Show minor mode, See Hideshow: (emacs)Hideshow, for hiding parts of proofs.
Except from the function hs-mouse-toggle-hiding bound to
<S-mouse-2>, the following useful functions are accessible
from the menu Hide/Show.
Hide all Mizar proofs in the article.
This means that instead of each top-level proof brackets like
proof ... end;, now ... end; or hereby ... end;,
you will see only three dots ... in the buffer.
The effect is actually very similar to that of creating an abstract
from the article, however, e.g. the top-level simple justifications
are still visible in the buffer.
This kind of hiding has no effect on proof checking, the file
is not modified by it. See section Proof checking, for commands that
disable proof checking of some part of the article.
Show a selected Mizar proof.
The first block following a point is shown.
After hiding some large portion of text
(e.g. by ‘hs-hide-all’), use this to completely unhide
the part you are working on.
Hide a selected Mizar proof.
The nearest proof block around the point is hidden.
Hide all subproofs of the current proof block.
This command is useful for getting overview of the proof, when
you are not interested in the detailed subproofs of its various
lemmas.
Show all of the article, cancel any hiding.
.
Toggle hiding/showing of a block.
See ‘hs-hide-block’ and ‘hs-show-block’.
Toggle hiding/showing of a block.
This command should be bound to a mouse key.
Argument E is a mouse event used by ‘mouse-set-point’.
See ‘hs-hide-block’ and ‘hs-show-block’.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Josef Urban on February 20, 2014 using texi2html 1.82.