The first line (alternatively: the file ending) of an .mmt file should allow adding configuration options.
If present, they change the behavior of the parser in a fundamental way but only in the current file.
Example options:
Delimiters: changing the delimiters so that .mmt files can be written by people who don't want to or can't type the special delimiters
Unicode: adding the lexing rule UnicodeReplacer (which automatically turns, e.g., -> into a Unicode arrow) so that .mmt files can be written in editors that don't make it easy to type Unicode symbols.
The first line (alternatively: the file ending) of an .mmt file should allow adding configuration options. If present, they change the behavior of the parser in a fundamental way but only in the current file.
Example options:
Delimiters: changing the delimiters so that .mmt files can be written by people who don't want to or can't type the special delimiters
Unicode: adding the lexing rule UnicodeReplacer (which automatically turns, e.g., -> into a Unicode arrow) so that .mmt files can be written in editors that don't make it easy to type Unicode symbols.