| Both sides previous revision Previous revision Next revision | Previous revision |
| using:vscode:settings [2024/10/19 19:06] – fponzi | using:vscode:settings [2025/11/04 09:29] (current) – fponzi |
|---|
| These settings are available in the Extensions → TLA+ section of the [[https://code.visualstudio.com/docs/getstarted/settings|Settings panel]]: | These settings are available in the Extensions → TLA+ section of the [[https://code.visualstudio.com/docs/getstarted/settings|Settings panel]]: |
| |
| * ''%%Java: Home%%'' allows to provide location of the JVM that the extension must use for running TLA<html><sup></html>+<html></sup></html> tools. | * ''%%Java: Home%%'' allows to provide location of the JVM that the extension must use for running TLA<sup>+</sup> tools. |
| * ''%%Java: Options%%'' allows to provide additional options that must be passed to the Java process when running TLA<html><sup></html>+<html></sup></html> tools. [[alygin/vscode-tlaplus/wiki/Java-Options|More details]] | * ''%%Java: Options%%'' allows to provide additional options that must be passed to the Java process when running TLA<sup>+</sup> tools. [[using:vscode:java_options|More details]] |
| * ''%%PlusCal: Options%%'' allows to provide additional options to the PlusCal transpiler. | * ''%%PlusCal: Options%%'' allows to provide additional options to the PlusCal transpiler. |
| * ''%%TLC Model Checker: Create Out Files%%'' defines if TLC model checker output should be sent to a .out file. | * ''%%TLC Model Checker: Create Out Files%%'' defines if TLC model checker output should be sent to a .out file. |
| * ''%%TLC Model Checker: Statistics Sharing%%'' allows to opt-in / opt-out sharing of TLC usage statistics. [[https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/util/ExecutionStatisticsCollector.md|More details]]. | * ''%%TLC Model Checker: Statistics Sharing%%'' allows to opt-in / opt-out sharing of TLC usage statistics. [[https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/util/ExecutionStatisticsCollector.md|More details]]. |
| * ''%%PDF: Convert Command%%'' specifies what command should be used to generate PDF documents from .tla files. | * ''%%PDF: Convert Command%%'' specifies what command should be used to generate PDF documents from .tla files. |
| | * ''%%PDF: Comments Shade%%'' enables a gray background on comments (the reminder for the line starting from the first \*.). |
| | * ''%%PDF: Comments Shade Color%%'' if Comments Shade is enable, allows you to choose the backgroud color. |
| | * ''%%PDF: No Pcal Shade%%'' disable the "comment" shading for pcal specifications. |
| | * ''%%PDF: Number Lines%%'' add line number on to the generated pdf file. |
| | |
| |
| ===== Other Useful Settings ===== | ===== Other Useful Settings ===== |
| These settings and configuration tricks are not provided by the extension itself, but leverage the general VS Code platform capabilities: | These settings and configuration tricks are not provided by the extension itself, but leverage the general VS Code platform capabilities: |
| |
| * [[alygin/vscode-tlaplus/wiki/Keyboard-Shortcuts|Keyboard Shortcuts]] | * [[using:vscode:keyboard_shortcuts|Keyboard Shortcuts]] |
| * [[alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing|Automatic Module Parsing]] | * [[using:vscode:automatic_module_parsing|Automatic Module Parsing]] |
| * [[alygin/vscode-tlaplus/wiki/Formatting-Preferences|Formatting Preferences]] | * [[using:vscode:formatting_preferences|Formatting Preferences]] |
| |
| | ---- |
| | <nspages -exclude -h1 -textNs="Browse Topics:"> |
fponzi