using:vscode:automatic_module_parsing

Automatic Module Parsing

The extension provides the TLA+: Parse module command for both translating a PlusCal algorithm to TLA<html></html>+<html></html> code and parsing the resulting TLA<html></html>+<html></html> 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.

  • using/vscode/automatic_module_parsing.txt
  • Last modified: 2024/10/19 21:13
  • by fponzi