The only unusual aspect of MMT’s default concrete syntax is the use of the characters ASCII 28-31 as structural delimiters. These are usually considered whitespace, and most fonts do not even have glyphs for them. Therefore, typing and displaying them depends on the editor and font used.
The advantage of these delimiters is that they do not clash with any other delimiters used by notations, lexing rules, or external formats that are integrated with MMT. Therefore, they permit near-perfect error recovery during parsing, orthogonality of language features, and combining different languages in the same file.
Every delimiter marks the end of a declaration or a component of a declaration.
|Symbol in jEdit||Delimiter||Name in ASCII||Marks end of||Comment|
|ASCII 29||Module Delimiter||Modules||any declaration that has nested declarations, i.e., theory, view, structure etc.|
|ASCII 30||Declaration Delimiter||Declarations||in particular includes and constants. Redundant if end of module follows|
|ASCII 31||Object Delimiter||Components of declarations||in particular type, definiens, notation of a constant. Redundant if end of declaration follows.|
Note that these form a hierarchy of nested levels and that we can think of SPACE as the 5th level delimiter, which marks the end of a keyword.
The jEdit plugin offers three ways to insert these non-standard symbols.
MMT adds buttons for all three delimiters to the toolbar of jEdit:
Plugins > MMTPlugin > Insert <DELIMITER>
jUS) for the object delimiter,
jRS) for the declaration delimiter,
jGS) for the module delimiter.
You can modify (or add new) abbreviations in
Extras > Global Options > Abbreviations.