2. Basic Functions

2.1 Running Mizar

C-c RET

mizar-it

C-c c

mizar-compile

Command: mizar-it &optional util noqr compil silent forceacc

Run mizar verifier on the text in the current .miz buffer.
Show the result in buffer *mizar-output*. If util is given, run it instead of verifier. If `mizar-use-momm', run tptpver instead. If noqr, does not use quick run. If compil, emulate compilation-like behavior for error messages. If silent, just run util without messaging and errorflagging. If forceacc, run makeenv with the -a option.

Command: mizar-compile &optional util

Run verifier (`mizar-it') in a compilation-like way.
This means that the errors are shown and clickable in buffer Compilation, instead of being put into the editing buffer in the traditional Mizar way. If util is given, call it instead of the Mizar verifier.

User Option: mizar-quick-run

Speeds up verifier by not displaying its intermediate output.
Can be toggled from the menu, however the nil value is no longer supported and may be deprecated (e.g. on Windows).

The default value is t.

User Option: mizar-show-output

Determines the size of the output window after processing.
Possible values: none, 4, 10, all.

The default value is 4.

User Option: mizar-goto-error

What error to move to after processing.
Possible values are none, first, next, previous.

The default value is "next".

2.2 Indentation and commenting

C-c C-c

comment-region

TAB

mizar-indent-line

M-C-\

indent-region

Command: comment-region

Comment each line in the region. With C-u prefix, uncomment each line in the region.

Command: mizar-indent-line

Indent current line as Mizar code.

Command: indent-region

Indent each nonblank line in the region.

User Option: mizar-indent-width

Indentation width for Mizar articles.

The default value is 2.

2.3 Error explanations and movement

C-c C-n

mizar-next-error

C-c C-p

mizar-previous-error

C-c C-e

mizar-strip-errors

Command: mizar-next-error

Go to the next error in a mizar text, return nil if not found.
Show the error explanation in the minibuffer.

Command: mizar-previous-error

Go to the previous error in a mizar text, return nil if not found.
Show the error explanation in the minibuffer.

Command: mizar-strip-errors

Delete all error lines added by Mizar.
These are lines beginning with ::>.