This shows you the differences between two versions of the page.
| Next revision | Previous revision |
| using:vscode:settings [2024/10/19 19:06] – created fponzi | using:vscode:settings [2024/11/12 17:50] (current) – fponzi |
|---|
| ====== settings ====== | ====== Settings ====== |
| This section provides the list of various settings that allow you to configure the extension to fit your preferences. | This section provides the list of various settings that allow you to configure the extension to fit your preferences. |
| |
| * ''%%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 ===== |
fponzi