Andrew Lygin

@magniff, you're right, this is the place where we could define the default value for the setting. Moreover, in some very early versions, it was set to `true`, but then...

When I just started working on vscode-tlaplus there were pretty severe restrictions on how an extension could use a terminal window, so I decided to use output channels instead. But...

You're right, in a couple of cases the extension doesn't capture boundaries of a PlusCal algorithm correctly. There's a quick fix for this particular issue, but unfortunately, it brings other...

Here it is: [Caveats](https://github.com/alygin/vscode-tlaplus/wiki/Caveats)

There's an attempt to improve VS Code highlighting capabilities: https://github.com/microsoft/vscode/issues/77133. I hope the result will allow us to fix this issue.

BTW, it's also better to keep the closing curly bracket on the last comment line: ``` (*--algorithm WriteStealing { { skip; } } *) ``` The extension starting with version...

@Alexander-N, I've fixed displaying of such error trace items, but TLC doesn't provide the exact action location, it points to the `INSTANCE` clause in the module being checked, so the...

Published in [v1.6.0-alpha.1](https://github.com/alygin/vscode-tlaplus/releases/tag/v1.6.0-alpha.1)

@ahelwer, you're right, TextMate grammar is not powerful enough to highlight such things. It's only possible with a full-featured parser. Maybe your tree-sitter grammar will make it to a TLA+...

I believe this feature is more general — one can jump from TLA+ to the corresponding PlusCal code block even when there were no errors. It would surely be good...