tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
357 stars 33 forks source link

Show model/spec name in VSCode status bar #285

Closed lemmy closed 1 year ago

lemmy commented 1 year ago

During the execution of TLC, you'll notice a rotating wheel adjacent to the "TLC" label located in the status bar. Additionally, the present specification and/or module's name should also be displayed.

https://github.com/tlaplus/vscode-tlaplus/blob/6eebff88f8cbb03358d9500e7d74760fb2dfaeed/src/commands/checkModel.ts#L295-L301