Introduction

This Eclipse plugin allows to edit files written in the Metamath language in the Eclipse IDE. It reuses the same core as MMJ2 and adds nice presentation.

Screenshots

Download

Here are links to the first versions of the Metamath Plugin for Eclipse: The change log can be found on GitHub
It's still in the early stages, please report any issue you have with installing / bootstrapping.

Installation

The plugin is compatible with Eclipse Oxygen. [download]
Currently, only the manual installation is possible: once the eclipse installation is finished, simply copy the emetamath plugin in the eclipse/dropins directory, or replace the previous version.

I've had issues with the size of the set.mm file (it's almost 35Mb). I had to add the following lines to file eclipse/eclipse.ini file: 
-Xms256m
-Xmx2048m
Simply find the lines starting with "-Xms" and "-Xmx" and replace them with those values. They specify the heap size allocated to Eclipse.

First Use

The Metamath Perspective

The metamath perspective allows to have direct access to all features provided by the plugin (views are setup and opened, wizard shortcuts are displayed, etc.). In order to activate the perspective, from the Window/Open Perspective/Others... menu, choose Metamath.

Creating a Metamath project

In order to create a new Metamath project, simply choose File/New/Metamath Project....
You'll be prompted for a project name.

Adding files to the project

You can add files to your project using the File/New/Metamath File... menu.
It is also possible to import an existing metamath file, ex. set.mm, either from the local system or from the metamath web site, by using the File/Import... menu, and selecting the respective Metamath File Import choice.

DONE: Fixed the long freeze times with set.mm. (cf. this article, eclipse bug 70412,etc.)
When loading the set.mm file itself, eclipse was hanging for a few seconds.

Setting the main file

In order to be compiled, a your project needs to know with which file to start, i.e. which is the "main" file. Other .mm file may then be included from this one.
You can set the "main" metamath file by choosing "set a main metamath file" from the contextual drop-down menu of the "Project Explorer" view.
The main metamath file is marked with a green triangle on the "Project Explorer" view.

TODO: Automatically tag the first metamath file added to a project as "main".

Features

The Project Explorer

The project explorer is a native eclipse view. The Metamath Plug-in enriches this view by marking the Metamath projects and files.

Project Properties

The project properties page allow the user to change the main metamath file, and the base URL to use when displaying Metamath proof explorer web pages in the internal web browser.

File Properties

The file properties allow to check whether a Metamath language file is currently the main metamath file or not.

The Metamath Editor

The Metamath Editor is used for editing files with the extension ".mm", written in the Metamath Language. It provides syntax highlighting, details about the label when hovering, an intelligent selection method through double-click, and a contextual menu giving access to the following commands:
  • Open Declaration - goes to the $c, $v or statement declaration for the selected metamath object
  • Open Notation (for symbols only) - goes to the notation axiom for the selected metamath symbol, ex. ctop
  • Open Definition (for symbols only) - goes to the definition axiom for the selected metamath symbol, ex. df-top
TODO: Enable "Open Notation" and "Open Definition" only when a metamath symbol is selected
TODO: Provide syntax highlighting also within comments, when correctly written ex. from ~ wtop or ` J `

Hover information

When the mouse stays over a metamath element for a short time, a tool tip appears, giving more information about that element.
DONE: Completed the information provided when hovering on a Metamath element: added element icon, name, hypothesis (for assertions), formula (for statements)
TODO: Also store the symbol's description when parsing Metamath language file, so that it can be displayed in the symbol's hover information

The Proof Assistant

To be completed.. (the buttons with "U" and "S" on the tool bar are the "unify" and "search unifiable assertions for this step" actions, respectively)

The Step Unification Selection View

The Step Unification Selection view enables to select a unification to be applied on a given step of the Proof Assistant view.
TODO: Enable the "Apply" action only when exactly one assertion is selected, or one of its children.
TODO: Allow the unification to take place also when clicking on the children nodes of a proposed unification.
TODO: Add other actions.
DONE: Corrected: When the proof worksheet was created from the "Open in Proof Assistant" action, and the proof worksheet is saved, the initial proof is used.
TODO: Correct: When the proof worksheet was created from the "Open in Proof Assistant" action, syntax highlighting is broken - has to do with line feeds.

The Proof Explorer View

The Proof Explorer view provides a quick way to locate or navigate through the metamath files. It shows the structure of the metamath project and its organization with chapters and sections.
TODO: Shall I rename the view in order to avoid confusions with the web page also named "Metamath Proof Explorer"?
TODO: Add the scoping statements in the Proof Explorer view ?
TODO: Add an action to export the proof back to the origin MM file, optionally in compressed format.
TODO: Filter out hypotheses, and keep only theoremes and axioms
TODO: Display formulas instead of statement descriptions

The Proof Browser View

The proof browser view is similar to the Metamath "Proof Explorer" web page. For a given proof, it displays in tabular format, one proof step per line, and for each proof step its name, hypothesis, reference, and resulting expression.
TODO: Also implement the "syntax breakdown" for axioms.
TODO: Also implement Chris Capel's "syntax breakdown" for axioms.

The Search View

TODO: Also search in the proof assistant worksheets ?

Project Properties

The project properties allow you to change the main metamath file in a project, the syntax coloring for the basic syntax types, and allows to enable/disable auto-transformations.
The Metamath project properties can be accessed through the Project contextual menu in the project explorer, or from the Eclipse menu under 'Project'.

Preferences

The Metamath preferences allow you to set the proof formatting (text mode formula formatting/TMFF), and the bracket highlighting properties. Metamath preferences can be accessed through the overall preference menu.

Source code

Source code can be found in GitHub.

On the To-Do list

TODO: Add help pages.
TODO: Add proper properties pages.
TODO: Build a bundle with eclipse, set.mm, and emetamath plugin to allow a one-shot download and install.