Caves Travel Diving Graphics Mizar Texts Cuisine Lemkov Contact Map RSS Polski
Trybiks' Dive Mizar Eddie YAC Software



Eddie::MSE vs. Mizar-MSE

Version History


Mizar-MSE Syntax

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.