Metamath Screenshots

If you have created a Metamath syntax highlighting file for another editor, let me know so that I can add it to this page. Contents of this page Visual Studio Kate Editor KEDIT Editor Vim and gVim Editors jEdit Editor gedit Editor Firefox Greasemonkey script for the Metamath web site Palm PDA Mnemosyne

Visual Studio    Xuanji Li published a Visual Studio Code extension [retrieved 1-Sep-2019] to support Metamath syntax highlighting. (Added 1-Sep-2019.)

Visual Studio screenshot

Kate Editor    The Kate editor [retrieved 1-Sep-2019] now has built-in Metamath syntax highlighting for *.mm files. Note "Metamath" in the lower right-hand corner. (Added 1-Sep-2018.)

Kate editor screenshot

KEDIT Editor    This is a screenshot of the ASCII database file "set.mm" (contained in the Metamath program download). For efficiency, the proofs in set.mm are typically stored in a compressed format that is hard for humans to read directly. (But if you want to try, the precise specification of the compressed format is given in Appendix B, p. 157, of the Metamath book.) The Metamath program is used to work with the proofs and can display them in several different ways, such as the web page 2eu5, which was generated with the command "show statement 2eu5 /html". The markup syntax for symbols, cross references, and bibliographic references in comments is described under the Metamath program commands "help language" and "help html".

Screenshot of theorem 2eu5 from set.mm in a text editor

Notes     The monospaced font in the editor screen is 8-point Andale Mono. The KEDIT editor is a product of the Mansfield Software Group. The syntax coloring is specified by a file called mm.kld, which is placed in KEDIT's USER directory.

* MM.KLD - KEDIT Language Definition for .mm (Metamath) files
:case
 respect
:identifier
[a-zA-Z0-9${}.=] [a-zA-Z0-9${}.=]
:comment
 paired $( $) nonest
:keyword
 ${ ALTERNATE 9
 $} ALTERNATE 9
 $d ALTERNATE 1
 $p ALTERNATE 1
 $v ALTERNATE 1
 $= ALTERNATE 1
 $. ALTERNATE 1
 $a ALTERNATE 1
 $e ALTERNATE 1
 $f ALTERNATE 1
 $c ALTERNATE 1

Vim and gVim Editors    David A. Wheeler created syntax highlighting files for Metamath source code in the Vim and gVim editors. (Added 7-Jul-2016.)

vim editor screenshot

gvim editor screenshot

Instructions: The README.md at https://github.com/david-a-wheeler/vim-metamath [retrieved 1-Sep-2019] explains how to install; just copy the files (for Unix/Linux into "~/.vim"; for Windows into ""%userprofile%\vimfiles").

jEedit Editor    Mario Carneiro created syntax highlighting files for Metamath source code and mmj2 worksheets for the jEdit editor. (Added 3-Jun-2014.)

jEdit editor screenshot

jEdit editor screenshot

Instructions: The XML files jedit-metamath.xml and jedit-mmj2.xml are the edit modes, and installation is just like any other jEdit edit mode. The XML files should be dropped into the C:\Program Files (x86)\jEdit 5.1.0\modes directory (appropriately modified for your installation directory), then the catalog file in this directory should be edited to add the lines:

<MODE NAME="metamath"        FILE="jedit-metamath.xml"
        FILE_NAME_GLOB="*.mm"/>

<MODE NAME="mmj2"        FILE="jedit-mmj2.xml"
        FILE_NAME_GLOB="*.mmp"/>

which enable interpretation of .mm and .mmp files using these two modes respectively.

gedit Editor    Steven Baldasty wrote a Metamath syntax highlighting [link broken 1-Sep-2009] file for the gedit editor. (Added 3-May-2009.)

gedit editor screenshot

Instructions: Copy the following code into a file called "metamath.lang" (or download it from Steven's site). Steven writes: "With gedit installed, download the metamath.lang attachment and move it to the folder where gedit stores its language files. On my Ubuntu laptop for example, I do this:

        sudo mv metamath.lang /usr/share/gtksourceview-2.0/language-specs

The next time you open a Metamath database, gedit activates the syntax highlighting automatically."

<?xml version="1.0" encoding="UTF-8"?>
<!--

 Copyright (c) 2009, Steven Baldasty <sbaldasty@gmail.com>

 Permission to use, copy, modify, and/or distribute this software for any
 purpose with or without fee is hereby granted, provided that the above
 copyright notice and this permission notice appear in all copies.

 Contributors:
    Steven Baldasty <sbaldasty@gmail.com>

 THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

-->
<language id="metamath" _name="Metamath" version="2.0" _section="Others">
   <metadata>
      <property name="mimetypes">text/mm</property>
      <property name="globs">*.mm</property>
   </metadata>
   <styles>
      <style id="keyword" _name="Keyword" map-to="def:keyword"/>
      <style id="comment" _name="Comment" map-to="def:comment"/>
      <style id="symbol" _name="Math Symbol" map-to="def:identifier"/>
      <style id="label" _name="Label" map-to="def:statement"/>
      <style id="include" _name="Path" map-to="def:constant"/>
   </styles>
   <definitions>
      <context id="scope" style-ref="keyword">
         <match>[$]+[}{]</match>
      </context>
      <context id="label" style-ref="label">
         <match>[A-Za-z0-9\-_.]</match>
      </context>
      <context id="comment" style-ref="comment">
         <start>[$]+[(]</start>
         <end>[$]+[)]</end>
         <include>
            <context sub-pattern="0" where="start" style-ref="keyword"/>
            <context sub-pattern="0" where="end" style-ref="keyword"/>
            <context ref="def:line-continue"/>
         </include>
      </context>
      <context id="proof" end-parent="true" style-ref="label">
         <start>[$]+[=]</start>
         <end>[$]+[.]</end>
         <include>
            <context sub-pattern="0" where="start" style-ref="keyword"/>
            <context sub-pattern="0" where="end" style-ref="keyword"/>
            <context ref="comment"/>
            <context ref="def:line-continue"/>
         </include>
      </context>
      <context id="statement" style-ref="symbol">
         <start>[$]+[cvdefap]</start>
         <end>[$]+[.]</end>
         <include>
            <context sub-pattern="0" where="start" style-ref="keyword"/>
            <context sub-pattern="0" where="end" style-ref="keyword"/>
            <context ref="comment"/>
            <context ref="proof"/>
            <context ref="def:line-continue"/>
         </include>
      </context>
      <context id="include" style-ref="include">
         <start>[$]+[\[]</start>
         <end>[$]+[\]]</end>
         <include>
            <context sub-pattern="0" where="start" style-ref="keyword"/>
            <context sub-pattern="0" where="end" style-ref="keyword"/>
         </include>
      </context>
      <context id="metamath">
         <include>
            <context ref="scope"/>
            <context ref="comment"/>
            <context ref="statement"/>
            <context ref="label"/>
            <context ref="include"/>
         </include>
      </context>
   </definitions>
</language>

Firefox Greasemonkey script for the Metamath web site    Charles Greathouse wrote a script to reformat and simplify the "This theorem was proved from axioms:" list on the Metamath Proof Explorer web pages. (Added in 2009.)

Greasemonkey script screenshot

Instructions: (1) In Firefox [retrieved 1-Sep-2019], install the Greasemonkey [retrieved 1-Sep-2019] add-on (click "Add to Firefox"). (2) Open the page for the beta version of the script [link broken 1-Sep-2019] and click "Install".

Palm Tungsten E PDA    Here is an experimental browser for Metamath on the Palm Tungsten E PDA. (Added 13-Oct-2006.)

Screenshot of experimental browser for Palm Tungsten E PDA

Mnemosyne screenshot    This is screenshot of the Mnemosyne [retrieved 1-Sep-2019] learning program, loaded with the output produced by the metamath program using the command "show statement ax-* /mnemosyne" (courtesy of Stefan Allan).

Screenshot of Mnemosyne