"Check and debug model with TLC" not enabled for MC.cfg

[lemmy]

The "Check and debug model with TLC" command is not available when the current editor shows a TLC config file.

[klinvill]

Should the "Debug a running model" command also be available then?

This should be a quick change, we only need to add || editorLangId == tlaplus_cfg to the appropriate when conditions in package.json

[alygin]

@klinvill, I think the "Debug a running model" command should not depend on the active file at all. But it should be disabled when there's already a TLC process runing. I mean, its when must be !tlaplus.tlc.isRunning.

But I don't know why this command provides the program parameter, which depends on the active file:

https://github.com/alygin/vscode-tlaplus/blob/3e268b53873a80db550d89f5a6b2b5cd1b812586/src/debugger/debugging.ts#L41-L47

@lemmy, could you, please, comment on that? Is it really required to provide the file path here?

[lemmy]

1) I can't think of a reason why I would need the file. On the contrary, the back-end sends the absolute path of the file to the front-end. 2) If the VSCode debug adapter supports concurrent debugger sessions, we don't have to disable "Debug a running model" if another TLC is already running.

[alygin]

1. I can't think of a reason why I would need the file. On the contrary, the back-end sends the absolute path of the file to the front-end.

I see that DebugConfiguration doesn't have the program parameter, yet you added it in the mentioned snippet. If it's not requred, we can remove it and allow the user to attach to a running TLC process from anywhere.

2. If the VSCode debug adapter supports concurrent debugger sessions, we don't have to disable "Debug a running model" if another TLC is already running.

In this case, the restriction is not on the VSCode debuging infrastructure side. VSCode doesn't allow opening two web view panels at once, that's why we should either disable the command, or support switching panels from one process to another.

[lemmy]

+1 for "attach to a running TLC process from anywhere".

When debugging, the web view panel doesn't provide much value. Thus, iff allowing concurrent debugger sessions is desirable functionality, it could probably do without the web view. On the other hand, a user can also start multiple VSCode instances.

[alygin]

Ah, sure, we don't display the result view while debugging, so it shouldn't be an obstacle.

[alygin]

It looks like the file path is not necessary when launching a debugger, so it can be used in more contexts.

[alygin]

The fix is available in the v1.6.0-alpha.2 pre-release.