Syntax highlighting, typechecking, and building for the MMT language.
-
Create a directory for your MMT archives (e.g., called
archives). -
Clone MMT archives into that directory (e.g., by
git clone https://gl.mathhub.info/MMT/urtheories.git urtheories). -
Open your
archivesdirectory in Visual Studio CodeOn Windows, you can do this by navigating to your
archivesdirectory using WIndows Explorer, right-clicking in an empty space there, and selectingOpen with Code. Alternatively and for other operating systems, open Visual Studio Code and selectFile -> Open Folder.... -
In the Visual Studio Code window you can now open arbitrary
*.mmtfiles. -
When you have an
*.mmtfile opened, you can press Ctrl+Shift+P to open the command pallette and seektypecheckandbuild.
In case of errors or bugs, a helpful command is Reload MMT.
Currently no code completion or lenses.
- Download the nightly build of this extension packaged as a
*.vsixextension file. - Open Visual Studio Code and press Ctrl+Shift+P (alternatively:
View -> Command Pallette...) - In the Command Pallette type
VSIXand select>Extensions: Install from VSIX.... - Select the
*.vsixextension file you downloaded in step 1.
- Added go-to-definition functionality for module references, including includes, structure domains, and specified meta theories
- Improved syntax highlighting of includes, rules, and explicit constants
- Fixed archives not being loaded on Windows (if they were on drives other than
C:), macOS and Linux derivates - Integrated a preliminary MMT shell
- Go To Definition functionality is now more fine-grained and only applicable on notations of a term (and not ambigiously on notations of its subterms)
- Go To Definition and Find All References support for MMT files
- no initial configuration necessary anymore: the extension comes now bundled with an
mmt.jarand automatically infers Java Home fromjavaonPATH
Minor updates of this README.
First version published to the Visual Studio Code marketplace.
