This section provides the list of various settings that allow you to configure the extension to fit your preferences.
These settings are available in the Extensions → TLA+ section of the Settings panel:
Java: Home allows to provide location of the JVM that the extension must use for running TLA<html></html>+<html></html> tools.Java: Options allows to provide additional options that must be passed to the Java process when running TLA<html></html>+<html></html> tools. More detailsPlusCal: 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. More detailsTLC Model Checker: Statistics Sharing allows to opt-in / opt-out sharing of TLC usage statistics. 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.These settings and configuration tricks are not provided by the extension itself, but leverage the general VS Code platform capabilities: