|
|
Eddie |
|
Eddie is an editor of Mizar articles.
Currently it''s available in two versions: for Mizar and for Mizar-MSE.
In the second case, the program also includes the checker - the module responsible for verifying proof correctness.
These are fully functional text editors
(multi-level undo/redo, search/replace with regular expressions, column blocks, etc.)
with the following aids for Mizarers:
- context sensitive help; press Ctrl+F1 on a reserved word -
this will display the respective topic (from the help file in Eddie::MSE and on the Mizar pages in Eddie::MIZ),
- context hints (after a click on an error, a hint describing that error is displayed in the status bar),
- positions of all issues are displayed on the right margin,
- navigation between reported issues (to the previous / next error, etc.),
- removing all errors,
- Mizar specific file extensions (*.abs, *.miz, *.voc, *.bib; also *.mse),
- syntax highlighting,
- running the verifier,
- running any of the detectors (irrelevant inferences, unused labels, etc.),
- running all or selected detectors,
- canceling a Mizar run,
- (un)indent doesn''t move labels and error descriptions that are in the first column of a line,
- (un)commenting blocks,
- right margin set to 79 characters.
Download programs Eddie::MIZ and/or Eddie::MSE.
Top
|
|
|
|