6. Browsing Functions

Mizar mode has tags for library references (theorems, definitions and schemes), vocabulary symbols, and constructors (see 4.1.1 Constructors and user symbols). They are produced for each new version of MML by the Library Committee, and reside in files "reftags" and "symbtags" in the abstr directory of the Mizar distribution.

There are several commands, keyboard and mouse shortcuts, to use them for searching and browsing.

Some other commands using symbtags need the complete constructor information to work. See section 9. Constructor explanations, for them.

M-;

mizar-symbol-def

<mouse-3>

mizar-mouse-symbol-def

<S-down-mouse-3>

mizar-mouse-direct-symbol-def

M-.

mizar-show-ref

<S-down-mouse-1>

mizar-mouse-direct-show-ref

M-*

pop-tag-mark

Command: mizar-symbol-def &optional nocompletion tag nootherw

Find the definition of a symbol at point with completion using file symbtags.
If in *.abs buffer, show its definition in current window, otherwise, i.e. in *.miz buffer, show it in other window. In the Completions buffer, aside from its normal key bindings, ';' is bound to show all exact matches. If invoked by right-click (`mizar-mouse-symbol-def'), second right-click does this too. nocompletion goes to the first hit instead. If tag is given, search for it instead. nootherw finds in current window. File symbtags is included in the Mizar distribution.

Command: mizar-mouse-symbol-def

<mouse-3> is bound to this function.
Runs mizar-symbol-def and the second mouse-3 shows the symbol's completions.

Command: mizar-mouse-direct-symbol-def

<S-down-mouse-3> is bound to this function.
Goes directly to the first match of the symbol under the mouse click.

Command: mizar-show-ref &optional nocompletion

Find the library reference with completion using file reftags.
Show it in its abstract in other window. Non-nil nocompletion goes to the first hit without completing. Library references are theorems, definitions and schemes imported from other Mizar articles. File reftags is included in the Mizar distribution.

Command: mizar-mouse-direct-show-ref

<S-down-mouse-1> is bound to this function.
Goes directly to the reference under the mouse click.

Command: mouse-find-tag-history

Popup menu with last 20 visited tags and go to selection.
Works properly only for symbols (not references).

Command: pop-tag-mark

Go back to where the last tag search was invoked from.

Command: symbol-apropos

Displays list of all MML symbols that match a regexp.

Command: mizar-bury-all-abstracts

Bury (put at the end of buffer list) all Mizar abstracts.
Useful when you did too much browsing and want to get back to your editing buffers.

Command: mizar-close-all-abstracts

Close all Mizar abstracts.
Useful when you did too much browsing and want to get back to your editing buffers.