| Next revision | Previous revision |
| using:vscode:commands [2024/10/19 18:53] – created fponzi | using:vscode:commands [2024/10/19 18:56] (current) – fponzi |
|---|
| | ====== Commands ====== |
| | |
| The extension provides the following commands in the [[https://code.visualstudio.com/docs/getstarted/userinterface#_command-palette|Command Palette]]: | The extension provides the following commands in the [[https://code.visualstudio.com/docs/getstarted/userinterface#_command-palette|Command Palette]]: |
| |
| * ''%%TLA+: Parse module%%'' for translating PlusCal to TLA<html><sup></html>+<html></sup></html> and checking syntax of the resulting specification. | * ''%%TLA+: Parse module%%'' for translating PlusCal to TLA<sup>+</sup> and checking syntax of the resulting specification. |
| * ''%%TLA+: Check model%%'' for running the TLC model checker on the TLA<html><sup></html>+<html></sup></html> specification. | * ''%%TLA+: Check model%%'' for running the TLC model checker on the TLA<sup>+</sup> specification. |
| * ''%%TLA+: Check model with non-default config...%%'' for running the TLC model checker on the TLA<html><sup></html>+<html></sup></html> specification. Lets the user select a non-default model config file. | * ''%%TLA+: Check model with non-default config...%%'' for running the TLC model checker on the TLA<sup>+</sup> specification. Lets the user select a non-default model config file. |
| * ''%%TLA+: Run last model check again%%'' for running TLC again without switching to the spec or model file. | * ''%%TLA+: Run last model check again%%'' for running TLC again without switching to the spec or model file. |
| * ''%%TLA+: Stop model checking%%'' for stopping currently running TLC process. The command is only available when a model checking is in progress. | * ''%%TLA+: Stop model checking%%'' for stopping currently running TLC process. The command is only available when a model checking is in progress. |
| * ''%%TLA+: Evaluate constant expression%%'' for evaluating an expression selected in the active editor. This command is also available in the editor context menu. | * ''%%TLA+: Evaluate constant expression%%'' for evaluating an expression selected in the active editor. This command is also available in the editor context menu. |
| * ''%%TLA+: Evaluate expression...%%'' for evaluating an arbitrary TLA<html><sup></html>+<html></sup></html> constant expression in the context of the currently open model. | * ''%%TLA+: Evaluate expression...%%'' for evaluating an arbitrary TLA<sup>+</sup> constant expression in the context of the currently open model. |
| * ''%%TLA+: Visualize TLC output%%'' for presenting model checking results. | * ''%%TLA+: Visualize TLC output%%'' for presenting model checking results. |
| * ''%%TLA+: Export module to LaTeX%%'' for generating a .tex and .dvi files from a TLA<html><sup></html>+<html></sup></html> specification. | * ''%%TLA+: Export module to LaTeX%%'' for generating a .tex and .dvi files from a TLA<sup>+</sup> specification. |
| * ''%%TLA+: Export module to PDF%%'' for generating a PDF document from a TLA<html><sup></html>+<html></sup></html> specification. | * ''%%TLA+: Export module to PDF%%'' for generating a PDF document from a TLA<sup>+</sup> specification. |
| |
| You’ll probably want to [[alygin/vscode-tlaplus/wiki/Keyboard-Shortcuts|add keyboard shortcuts]] to some of these commands, or even make them [[alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing|run automatically]]. | You’ll probably want to [[alygin/vscode-tlaplus/wiki/Keyboard-Shortcuts|add keyboard shortcuts]] to some of these commands, or even make them [[alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing|run automatically]]. |
| |
| |
fponzi