Caves Travel Graphics Mizar Articles Cuisine Contact Polski

Base Mizar YAC Software

Back Eddie Mizar-MSE Syntax MIZAR 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. A brief version history: Version 0.33: Additions: #29 - added hints for errors reported by Mizar, #81 - added the option of canceling a Mizar run (or detectors), #93 - added context help for errors reported by Mizar, #146 - before mizaring, the file name is checked (so that it is consistent with Mizar requirements), #148 - (un)indent doesn't move labels is now an options in the preferences (see #113), Fixes: #149, #150 - small fixes in block handling, #2, #3, #40, #76, #123, #151 - various fixes in search / replace functionality, #14, #60, #86, #124, #126, #147 - other small fixes. Version 0.32: #113 - (un)indent doesn't move labels and error descriptions that are in the first column of a line, #103..#108, #114..#116, #120, #122 - various smaller editor fixes. Version 0.31 - fixes: #96 - overwrite mode stopped working after the change to SynEdit 2.0.5, #97 - text selection with a mouse was working incorrectly after the change to SynEdit 2.0.5, #98..#102 - various smaller issues relating to Mizar and YMK interop. Version 0.30: Additions: #17 - dialog window for choosing which detectors to run (Eddie::MIZ), #22 - after running the verifier or detector(s) the number of found issues is displayed, #35 - change the order of windows in the windows toolbar, #38 - register extensions handled by these programs, #39 - drag and drop documents into Eddie, #9, #47 - toolbar enhancements, #80 - positions of all issues are displayed on the right margin, #92 - context sensitive help for reported issues (Eddie::MSE). Fixes: #5 - irrths and irrvoc sometimes report errors in the wrong line (Eddie::MIZ), #70 - smart unindent turned off, #79 - AV on file close, #82 - trailing spaces are trimmed in editing operations, #90 - forced single instance of the application. Version 0.23 - fixes: #1 - typing a file name without an extension, when trying to open an article, causes an error, #45 - when opening a file from the command line, menus and toolbars remain disabled, #72 - when choosing the first topic through Ctrl+F1, nothing happens (Eddie::MIZ), #73 - syntax help updated to go to new syntax pages (Eddie::MIZ), #74 - update list of reserved words in the highlighter (Eddie::MIZ). Version 0.22: I added my own article to the download: "Boolean Properties of Sets" (SETS.mse). Additions: infix notation for predicates in Eddie::MSE, context sensitive help in both Eddie::MSE and Eddie::MIZ; 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), better help in Eddie::MSE. Fixes: #50 - remove all issues didn't clear issue descriptions at the end of the article (Eddie::MIZ), #52 - article verification didn't set the modification flag on a file (Eddie::MSE), #56 - reserved words written in upper case were also highlighted (Eddie), #57 - after running the verifier, the last empty line of a file was deleted (Eddie::MSE), #61 - ANALYZER - internal error 999 when not contradiction was under a quantifier (Eddie::MSE), #62 - ANALYZER - error 48 was not reported for local constants in diffuse statements, if another diffuse statements was placed between the constant's introduction and its use (Eddie::MSE). Version 0.21 - Eddie::MSE: An article by Wojciech Trybulec: "Axioms of Incidence" (WAT.mse) was added to the download. Plus fixes: #31 - keep cursor position when running Mizar, #41 - errors not reported when an unregistered type is used in the reserve...for instruction, #42 - CHECKER errors are reported at EOF, not at their positions, #44 - removed limit on identifier length (16 characters). Version 0.20 - Eddie::MSE a second program for Mizar-MSE, that includes the Mizar-MSE checker, English help file that described reserved words and symbols, and error messages, instructions added to the processor: "type" and "pred" that are used to introduce types and predicates respectively, Mizar-MSE specific file filters (*.mse). Version 0.10 - Eddie::MIZ a fully functional text editor (multi-level undo/redo, search/replace with regular expressions, column blocks, etc.), Mizar file filters (*.abs, *.miz), syntax highlighting, running the verifier, running any of the detectors (irrelevant inferences, unused labels, etc.), running all detectors, (un)commenting blocks, multilingual (Polish-English), right margin set to 79 characters. Prehistory: Various versions of the editors for Mizar-MSE and Mizar I started writing in 1989 (circa about). I wrote then the first version of Eddie (for Mizar-MSE) in Turbo Pascal 5 (+/- 1), still before the Turbo Vision library. It wasn't an MDI program - it was based on the look & feel of Borland's products. In the next couple of years, I wrote new versions of the editor (renamed later to PC-MSE) that were distributed by Schola and were used to teach mathematics at the University of Bialystok. There was even a program to set the application's colors: :-) After trying with Mizar-MSE, I started to write a larger, MDI-like editor, but still before the Turbo Vision library. It's name was Deep Thought (some of you may notice that both names - Eddie and Deep Thought - were taken from the phenomenal *book* "The Hitchhiker's Guide to the Galaxy" :-) ), it had syntax highlighting, a .voc editor and other functions helpful for writing Mizar articles. Unfortunately, through all these years, I lost the sources as well as the program... In 1998 I rewrote Eddie in Delphi and took to other things for a long time. But at the beginning of 2007, I returned to the project, and so the above mentioned versions were born. Top