3. Summaries and Hide/Show

C-c C-r

make-reserve-summary

C-c C-z

make-theorem-summary

Command: make-reserve-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.

Command: make-theorem-summary

Make a summary of theorems in the buffer *Theorem-Summary*.
Previous contents of that buffer are killed first. The command `hs-hide-all', accessible from the Hide/Show menu, can be used instead, to make a summary of an article.

3.1 Hide/Show - Hiding proofs

<S-mouse-2>

hs-mouse-toggle-hiding

Mizar Mode customizes the standard Hide/Show minor mode, See Info file `emacs', node `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.

Command: hs-hide-all

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 5.1 Proof checking, for commands that disable proof checking of some part of the article.

Command: hs-show-block

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.

Command: hs-hide-block

Hide a selected Mizar proof.
The nearest proof block around the point is hidden.

Command: hs-hide-level

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.

Command: hs-show-all

Show all of the article, cancel any hiding.
.

Command: hs-toggle-hiding

Toggle hiding/showing of a block.
See `hs-hide-block' and `hs-show-block'.

Command: hs-mouse-toggle-hiding

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'.