The MMT API provides a number of extension interfaces that permit injecting code for customizing the behavior of MMT algorithms.
All extensions are persistent and have full access to the MMT controller.
All extensions inherit from
info.kwarc.mmt.api.frontend.Extension and can be studied by browsing the known abstract subclasses in the API documentation.
The API also includes numerous concrete extensions. Some of these are loaded by default, some are loaded on demand, some can be added manually at run time.
To write an extension, simply subclass the desired extension interface in Java or Scala.
The subclass must have a single constructor that takes no arguments.
It may override the
destroy methods to perform arbitrary code during initialization and destruction.
The former also receives a list of strings as arguments, which users can pass when registering the extension.
There is a wide variety of extension interfaces. They are documented in the respective API documentation pages, which are linked here.
Therefore, this page only gives an overview of their functionality:
MMT breaks the main processing pipeline of any formal language implementation into the following phases
parser.Parsers convert character streams into MMT data structures. This includes at least lexing, parsing, and management of notations, but may included full-fledged type-checking.
checking.Checkers analyze and transform the MMT data structures returned by parsing. This includes type-checking and inference of omitted parts (often called reconstruction, elaboration, refinement).
checking.Interpreters bundles parsing and checking into a single step, often by combining the available parsers and checkers.
uom.Simplifiers perform computations and rewriting as well as transforming content by elaboration. These are often intertwined with checking.
presentation.Presenters transform MMT data structures into human-oriented formats, such as the original syntax or HTML.
Further steps in this pipeline that are designed but not maturely realized yet include theorem proving, code generation, and execution and compilation of programs.
Each of these steps is actually split into two interfaces: one for the structural levels and one for objects (see central concepts for the difference). That allows combining, e.g., MMT’s default object parser with a new structure parser.
frontend.ChangeListeners add general purpose change-listening functionality. The methods of these extensions are called when MMT content is added, updated, etc.
web.ServerExtensions allow using MMT as a very convenient web framework by adding interface functins to the HTTP server. Each extension has a
keyand serves requests to the URL
Various extensions for fine-grained customization:
frontend.Plugins add language-specific functionality and are automatically loaded when the respective MMT theory is loaded.