Markus Alexander Kuppe

For starters, we would even need to figure out the module name from the current editor location. Instead, adding all reachable (from the root spec) modules in VSCode's `Ctrl+O` should...

@peterzeller Do you need more input?

@peterzeller Thanks for the update! :-) 1. I suggest extending `SanyStdoutParser`. LSP might strategically be the preferred (@alygin had reasons not to use LSP), and the TLA+ debugger indeed introduced...

FWIW: https://github.com/alygin/vscode-tlaplus/blob/775dbf770a0a182341b68e5af91e5b34965fae0e/src/commands/checkModel.ts#L240-L241 is another use-case where access to SANY's AST would be useful.

From personal experience, it would be convenient to always include the most recent TLC build--even better if a TLC build would trigger a nightly build here (like the eclipse toolbox...

Independently of this discussion, I'd suggest removing `tla2tools.jar` from the repository strategically. The jar file is > 2MB now, and we've wanted to do more frequent TLC releases anyway. Also,...

This feature is for those who have seen SCMs come and go or who have experienced specs being moved around; others can turn it off (like it is possible in...

Re, debug-adapter-protocol. Prototype implemented with https://github.com/lemmy/vscode-tlaplus/commit/6752f0076274655a706e3229916232ca0ae5423d From a UX perspective, the launch buttons on the editor alone/independent of the debugger would be a nice addition. 

There is already TLC's config file (`YourSpec.cfg`), and I don't think TLA+ values should be persisted as project-level VSCode settings. Perhaps, it would be useful to generate a more complete...

http://tla.msr-inria.inria.fr/kuppe/vscode/ hosts builds of vscode-tlaplus with the most recent nightly build of TLC. If one adds ```-generateSpecTE``` as a TLC command-line parameter in vscode-tlaplus, TLC will create ```SpecTE.tla``` after model...