In this tutorial, we show how to build a few minimal applications on top of the MMT library. We will not build the applications step by step. But they are chosen to be easy to understand, reproduce, and play with. They cover various but not all of the extension interfaces that MMT provides to application developers.
The following assumes that
This mini-application shows how to easily integrate MMT with HTML pages. It uses
First we start an MMT server:
server on 8080
Now download the file src/mmt-api/resources/mmt-web/editing-example.html which is provided as part of the MMT sources.
Opening the file in a browser shows two input fields for
Clicking the commit button shows the same expression in MathML obtained by
Best results of MathML display are obtained in Firefox.
The html file is self-documenting. Open it in a text editor to see how it works.
You can also use your browser’s inspector to see the Ajax request and response that the submit button generates.
This mini-application shows how to use MMT as an editor for OpenMath content dictionaries. It uses
Concretely, it exports MMT theories as content dictionaries.
Consider the archive
MMT/examples, which was cloned automatically during setup.
In it, consider the files in the folder
Enter the commands
extension info.kwarc.mmt.openmath.Exporter build MMT/examples openmath http..cds.omdoc.org/examples/tutorial
The first command registers the exporter with MMT. There are several ways to automate this registration. For example, you can script MMT by putting the commands in an
msl file or permanently add the exporter by adding an entry to your
The second one runs the build target all theories:
contentfolder, which are organized by their URI. Therefore, we restrict it to the folder
http..cds.omdoc.org/examples/tutorialto export all theories of the tutorial.
export/openmath/contentof the archive.
The types and definitions are used to generate FMPs. The meta-data key
@_description is used to give descriptions.
The implemenation is part of the MMT sources in the project
The only file of this project is src/mmt-openmath/src/info/kwarc/mmt/openmath/Exporter.scala.
It is self-documenting.
This mini-demo uses explores how to extend MMT’s semantics by dynamically adding rules. It uses
Consider the file
tutorial/3-literalsrules.mmt in the archive
It defines the natural numbers and then adds two kinds of rules:
scala_realizations/info/kwarc/mmt/examples/tutorialof the archive and added to the theory using the
Computation rules is already part of MMT’s core algorithms. This application has to add new ways for adding computation rules dynamically. The implementation is not presented as a minimal example. Instead, we provide links to code in the main MMT packages.
ruleis added by a ParserExtension that is part of the core MMT code and that is loaded by default. It is defined in the file src/mmt-api/src/main/info/kwarc/mmt/api/symbols/RealizedConstant.scala.
role Simplifyis picked up by the ChangeListener defined in the file
[https://github.com/UniFormal/MMT/blob/master/src/mmt-lf/src/info/kwarc/mmt/lf/SimplificationRuleGenerator.scala](src/mmt-lf/src/info/kwarc/mmt/lf/SimplificationRuleGenerator.scala). It inspects the type of each new constant with the appropriate role, generates a rule, and adds it to the theory.