Show command "Check model with TLC" even when the model checking panel has focus

[lemmy]

The "Check model with TLC" command is not shown when the model-checking panel has focus. This makes it necessary to e.g. close the panel if a user wants to add new options (via the new prompt).

/cc @klinvill

[klinvill]

@lemmy I whipped up a quick additional command ("TLA+: Run last model check with new options") that should work when the model checking pane was focused. Feel free to give it a whirl and let me know if it works well for you.

Ideally we could just also enable the tlaplus.model.check.run command (which shows up as "TLA+: Check model with TLC" in the command pane) when the model checking pane is open, but I wasn't able to find a good way to do it that doesn't involve manually setting the context. I'd rather not manage additional context if we don't have to so I opted to introduce a new command.

[lemmy]

@klinvill Thanks; I will report back on the ergonomics.

[alygin]

I'd rather not manage additional context

@klinvill, why don't you like this approach? We already have a couple of contexts. To me, this looks like the right way to implement the feature.

[alygin]

BTW, it looks like we don't need an additional context, we can reuse tlaplus.tlc.canRunAgain to enable the command.

[klinvill]

Ah excellent point, I should have realized that when I used tlaplus.tlc.canRunAgain as the condition for the new command.

Unfortunately there's a second challenge with re-using tlaplus.model.check.run since the checkModel() function either expects a file URI to be passed or pulls the URI from the active editor file. If we wanted to reuse this function, we would have to turn the flow into something like:

1. If given a file URI , read the spec from the file.
2. If the active file is a TLA+ file, read the spec from that file.
3. If lastCheckFiles is populated, use that spec.
4. Error, no spec to check

This is definitely feasible, but the warning messages for no active file editor or the active file not being a .tla or .cfg file are coded into the checks with those functions. So the three options I see are:

• Use a new command (the check again with options command I introduced)
• Re-use the old command and move the warning messages (for no active editor/no TLA+ file) outside of the check functions (getActiveEditorFileUri() and getEditorIfCanRunTlc())
• Re-use the old command and refactor the check functions to return result types that can include the error message in them.

I think the 3rd option is the cleanest, but requires introducing result types that aren't used elsewhere (or throwing and catching exceptions). In light of that, my preferred approach is still the first option: a new command. @alygin which approach do you think we should take?

[alygin]

I'd pursue the 3rd option with introducing a result type and minor refactoring.

I think adding a new command for this specific case doesn't look justified. A new command would add nothing to the existing one in terms of functionality, so we can just expand the context of "Check model with TLC", and shorten the user path a little bit.

[lemmy]

3. seems to be most in line with how the Toolbox handles its F11 shortcut.