The MMT Shell
The MMT shell is invoked by running mmt.
The language of shell commands is implemented by the
Each subclass comes with scaladoc and can be best understood by browsing the known subclasses in the API documentation.
The up-to-date context-free grammar for shell commands is part of the constructor parser in the companion object
Action and can be best understood by reading the source code.
ANSI Formatting in the MMT Shell
Some shell output uses ANSI escapes for highlighting. To display the formating, you can use ansicon for the windows console or ansi console for the eclipse console. (Both are optional and very easy to install and use.) Unix shells should understand it natively.
An MMT script is a text file containing one shell command per line. (Empty lines are allowed, lines starting with // are ignored.)
The customary file ending for MMT scripts is
These scripts can be run with the file command below.
Individual Shell Commands
The following documents some important individual commands. This documentation uses upper case names for argument types. Some common argument types are:
FILE: a file name (relative to the current directory)
FOLDER: a folder name (relative to the current directory)
U: an MMT URI (relative to the current base URI)
STRING: a string
exit: exits MMT (releases all resources and terminates all spawned threads).
extension STRING: registers the extension whose qualified Java class name is
STRING. The class must be on the class Java path already.
base URI: sets the base URI to U.
scala: drops to the scala shell. Within the scala shell, some special features are available:
- The variable controller is bound to the MMT controller, which gives users full access to the internal MMT state.
- MMT interpolations is active: for example, the string
TERMas an MMT term and returns the resulting object.
See log for the logging model.
log console: adds standard output as a logging receiver.
log file FILE: adds the file FILE as a logging receiver.
log filets FILE: as above but adds timestamps to all log messages.
log+ STRING: switches logging on for the component with id STRING.
log- STRING: switches logging off for the component with id STRING.
Defining make-style targets
file FILE [STRING]: runs the shell file
FILE(which in particular registers all macro definitions in FILE); if provided, immediately runs one of those macros.
define STRING: begins the definition of a named macro.
end: ends the current macro definition.
do STRING [FOLDER]: runs the previously registered macro (FOLDER can be used to disambiguate between multiple macros of the same name defined in different folders)
Working with MMT content
MMT reads content automatically by searching for the needed MMT URI on the math path (see below). Therefore, there are only a few commands for directly accessing content.
read FILE: reads a file into memory. Usually this is not necessary because resources are read automatically on demand.
get U [CONTENT] [PRESENT] OUTPUT: retrieves the resource with MMT URI
Uand applies various operations to it. This command is largely superseded by the HTTP interface but occasionally useful to run on the shell.
- omitted: simply retrieves
closure: computes the dependency closure of U and retrieves all elements in it
Uand elaborates it
component STRING: retrieves the component
- omitted: simply retrieves
- omitted: presentation as text
present STYLE: presentation using the style
write FILE: write to file
window STRING: output to a separate window with id
STRING. If the id has not been used before, a new window is created; size and position of the created windows can be controlled by other shell commands
respond: no output (useful for programmers who wish to access the result programmatically)
navigate U: does nothing itself but sends the navigation event to all registered change listener extensions, which include the GUI (if started).
clear: removes all content from memory.
The Math Path
The math path maintains a catalog that maps MMT URIs to physical locations. Several commands exist to add entries to the math path.
mathpath archive FILE: adds the location of an MMT archive. The path is searched recursively and registers all found archive folders and mar files.
mathpath local: adds the local file system, i.e., file:// URIs are mapped to themselves.
mathpath fs FILE U: adds a catalog entry that maps every URI of the form
U/RESTto the physical location
FILE/RESTon the local file system.
mathpath java FILE: adds a catalog entry for modules written directly in Scala/Java. URIs are interpreted as fully qualified Java class names.
Archives and Building
archive ID relational: loads the relational knowledge into memory.
build ID TARGET: runs a build target. See the documentation of the build tool for details on running build commands on archives.
oaf root FOLDER URI: sets a local folder as the root for git-clones of archives in the OAF.
oaf clone GROUP/REPOS: git-clones the archive
FOLDER/GROUP/REPOSand recursively clones its dependencies.
oaf pull: git-pulls (git pull origin master) all repositories in
oaf pushes: git-pushes all repositories in
oaf setremote: configures the remote URI of all repositories in
FOLDER(useful to switch from https to ssh or when the location of the server has changed).
remote ID COMMAND: executes a command on a remote MMT client that connected via the remote admin extension
web.RemoteActionServer for details.