Automatic Module Parsing

The extension provides the TLA+: Parse module command for both translating a PlusCal algorithm to TLA⁺ code and parsing the resulting TLA⁺ module. This command is so important in the specification writing process that you might want it to be executed every time you save a .tla file to get quicker response.

There’s a simple way to do that:

1. Open the Command Palette and execute the command Preferences: Configure Language Specific Settings... → TLA+.
2. Set the source property of the editor.codeActionsOnSave setting to true. The final result should look like this:

    "[tlaplus]": {
        "editor.codeActionsOnSave": {
            "source": true
        }
    }

That’s it. From now on, every time you save a .tla file the extension will automatically run the TLA+: Parse module on it and report errors if there any.

---