The type checker treats any occurrence of _ in MMT terms as a fresh unknown and tries to infer its value. This turns the system into a (very simple) interactive theorem prover. Options of the latter kind will, when selected, introduce new hole-terms for the arguments. This includes forward-search (generate closed terms of the right type) and backward-search (find functions that when applied return the right type). If the cursor is placed just before a hole-term, auto-completion runs the MMT theorem prover for a small depth and suggests terms that have the right type. Type-checking treats it like an unknown term of type T. By default it is triggered by CTRL-Space.īasic auto-completion shows a list of constants that are currently in scope.īut in conjunction with hole-terms, MMT performs unification to provide typing-aware auto-completion.Ī hole-term is a term of the form ≪T≫ for a type T. Auto-Completion and Hole-TermsĪuto-completion is provided and can be configured via the Sidekick plugin. The normalize command fully computes the selected expression and shows the result. If this gets stuck, MMT can be safely interrupted by pressing MMT’s stop button. This is called by Sidekick (see below), and the Sidekick options for the MMT mode allow configuring when type-checking occurs. MMT files are automatically processed using the MMT parser and type-checker. Changes to its text style are ignored and overwritten. It is assigned to all hidden, i.e., invisible, parts. The token type COMMENT4 is reseved by MMT. Additionally, the token types LITERAL1 to LITERAL4 are assigned to brackets at different levels. Most importantly, the mode assigns the token types OPERATOR and KEYWORDn. Other mode-specific options including the appearance of the syntax highlighting can be configured via the generic jEdit options dialog. mmt files, which provides syntax highlighting. See Global Options - Shortcuts for the list of actions (or if you want to see the internal names, which can be entered, e.g., in the jEdit Action bar).

Most commands are internally realized as jEdit actions, and these actions can be called in a variety of user-customizable ways. predefined keyboard shortcuts (see Global Options - Shortcuts and select the MMT Plugin).the group of MMT-related buttons in the toolbar.the MMT group in the context menu when editing an MMT file.Unless otherwise mentioned, functionality that requires explicit human interaction can be triggered in several ways: Installation instructions can be found here Functionality The jEdit IDE allows to enter and edit MMT content manually.

Jedit console plugin