using:vscode:settings

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Settings ======
This section provides the list of various settings that allow you to configure the extension to fit your preferences.

===== Extension Settings =====

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<sup>+</sup> tools.
  * ''%%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.
  * ''%%TLC Model Checker: Create Out Files%%'' defines if TLC model checker output should be sent to a .out file.
  * ''%%TLC Model Checker: Options%%'' allows to provide additional options to the TLC model checker. This setting supports variables ''%%${specName}%%'' and ''%%${modelName}%%'' that are automatically substituted to the .tla and .cfg file names (without extensions) respectively. [[https://github.com/tlaplus/tlaplus/blob/master/general/docs/current-tools.md#command-line-options|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: 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 =====

These settings and configuration tricks are not provided by the extension itself, but leverage the general VS Code platform capabilities:

  * [[using:vscode:keyboard_shortcuts|Keyboard Shortcuts]]
  * [[using:vscode:automatic_module_parsing|Automatic Module Parsing]]
  * [[using:vscode:formatting_preferences|Formatting Preferences]]

----
<nspages -exclude -h1 -textNs="Browse Topics:">