Run TLC in VSCode integrated terminal

[lemmy]

Some TLC-specific TLA+ operators such as PickSuccessor prompt users for (interactive) input (on stdin). This is currently unsupported because the extension just prints TLC's stdout/stderr to the output section of the model-checking results webview (check-result-view.html) and expects no input. I suggest changing the extension such that it (also) creates a proper VSCode terminal (not just read-only OutputChannel) with which a user can interact with TLC.

Long-term, this might be a use-case for the debug adapter protocol.

[alygin]

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 VSCode 1.37 introduced a terminal API (example), so I think it should be possible to switch to it.

As for the debug adapters, I watched your screencast, and I think it would be great to have such feature. Yet I didn't have time to dig into it, and understand how different components must interact to provide proper debugging experience.

[lemmy]

Re, debug-adapter-protocol. Prototype implemented with lemmy@6752f00 From a UX perspective, the launch buttons on the editor alone/independent of the debugger would be a nice addition.