Skip to content
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
71 lines (62 sloc) 4.88 KB
* Added a new search command for listing (directly or indirectly) incomplete proofs
* Added support for main Metamath file within sub-directories of the project directory
* Added support for setting custom working variable prefix in the Project Property page
* Added support for setting "statement type" in the Project Property page
* Fixed the issue that proof unification/step selection was not working properly anymore after changing MM files.
* Fixed opening a theorem as a "new" proof if its compressed proof is empty, to avoid error message.
* Fixed clean up of messages before a rebuild.
* Added ability to add/remove types, and change their colors in the Project Property page
* Fixed exception when changing Project main file
* Added "Verify Proofs" menu to the Metamath menu.
* Fixed "MMT Folder not specified" issue.
* Fixed position for some error messages
* After unify action, reposition cursor at the previous location.
* Added a "toggle comment" command in the proof editor.
* Added autoTransformations and deriveAutocomplete to speed up proof assistant
* Corrected issues when opening a metamath file outside of the metamath perspective
* Fixed "Search References" action
* Fixed positions for some messages
* Added highlighting of the matching bracket, and corresponding preference on the preference page
* Fixed the key bindings : Ctrl-U now launches the unification, like in MMJ2.
* Re-integrated with the latest MMJ2 (Source, MessageHandler, Progress, etc. )
* Fixed hover tooltip sizes
* Improved progress monitor during the loading / parsing of Metamath files
* Warning: Locations of many errors are not available anymore, or not correct. These will have to be corrected later on.
* Added a "Export Proof" action to re-export complete proofs to metamath files.
* Added annotations to the Proof Assistant Editor (symbols in the margin + position highlighted).
* Started a skeleton for incremental build (to only parse/verify the part of the metamath files which have changed)
* It is not necessary anymore to "save" in the Proof Assistant before unification.
* Added a Project Properties page, including "Main File" and "Proof Explorer Web Base URL" properties
* Added a tool bar to the Proof Browser View, with current theorem name, back and forward button.
* "Type" constants (wff, |-, set, class) are now colored in gray, like in Metamath web pages
* Added project properties for defining the "type" constants (in, these are "wff", "set" and "class"), and their colors
* Added the "unify & renumber" action (in menu, context menu and toolbar)
* The Proof Browser view now also shows syntax breakdown for axioms.
* Added a Proof Browser view, similar to the Proof Assistant, but in tabular format, and not editable (still to be polished).
* Added the "Internal Web Browser View" in the "Show In" context menu: this enables to browse the (www)
* Filled in the "Show In" menu of the "Proof Explorer View"
* Completed the information provided when hovering on a Metamath element: added element icon, name, hypothesis (for assertions), formula (for statements)
* Hover information now also appears in Metamath Proof Assistant editors
* Added two new contextual commands "Add Block Comment" and "Remove Block Comment" to (un)comment a section of Metamath language ($ replaced by @)
* Added an acknowledgement message (and conformed to GPL) by adding an "about" message. It can be accessed through Help/About Eclipse/Plug-in Details, selecting "Metamath" plugin, and pressing "Legal Info".
* Corrected: A proof opened from a Memamath file using the contextual menu "Open in Proof Assistant", modified and saved as .mmp now does not loose anymore the modifications and cursor position.
* Improved speed by replacing the Syntax Colorer (PresentationReconciler) by a faster one, which colors only the current viewed text
* Started a "Metamath Search Page" (accessible through the "Search/Search..." menu), though it is not functional yet
* Checked compatibility with Eclipse 3.2 :
would have to remove references to WizardNewProjectCreationPage.getSelectedWorkingSets, StyledString, IStyledLabelProvider, and ITextHoverExtension2
* "Metamath" Menu now appears only when a Proof Assistant editor is active.
(the corresponding toolbar buttons "Unify" / "Step Selection" will stay because of
* Hover hints are now also available on proofs.
* Replaced "Outline" by "Proof Explorer" in the "Show In" menu of the Metamath Search page (indeed, the Metamath plugin does not provide any outline)
* Removed the "Console" view from the perspective, as it is currently not used. (You can reset your perspective to default using "Window/Reset Perspective")
* Initial release
You can’t perform that action at this time.