-
Notifications
You must be signed in to change notification settings - Fork 31
Automatic Module Parsing
Andrew Lygin edited this page Jul 25, 2020
·
7 revisions
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 theeditor.codeActionsOnSave
setting totrue
. 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.