You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
Open the Command Palette and execute the command Preferences: Configure Language Specific Settings... → TLA+.
Set the source property of the editor.codeActionsOnSave setting to true. The final result should look like this:
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.