====== Automatic Module Parsing ======

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

  - Open the [[https://code.visualstudio.com/docs/getstarted/userinterface#_command-palette|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:

<code json>
    "[tlaplus]": {
        "editor.codeActionsOnSave": {
            "source": true
        }
    }
</code>

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.