Enable check model command from model checking panel

[klinvill]

Addresses #215, replaces #216.

This PR extends the tlaplus.model.check.run command to be enabled whenever tlaplus.tlc.canRunAgain is true. This has the effect of showing the check model command when the model checking pane is active. When no TLA+ file is active, the command falls back on using the last checked spec. The flow of the checkModel function roughly follows:

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 PR also refactors the helper functions called by checkModel to return Result types. Returning a Result allows the error messages to be ignored in the case where a TLA+ file is not active but the last checked spec is known and can be used.

As part of the refactoring, I also extracted the canRunTlc() checks from functions that get the editor and moved them to the functions that run the TLC tool (doCheckModel() and doEvaluateExpression()).

[sonarqubecloud[bot]]

Kudos, SonarCloud Quality Gate passed!

0 Bugs
0 Vulnerabilities
0 Security Hotspots
1 Code Smell

No Coverage information
0.0% Duplication

[sonarqubecloud[bot]]

Kudos, SonarCloud Quality Gate passed!   

0 Bugs
0 Vulnerabilities
0 Security Hotspots
1 Code Smell

No Coverage information
0.0% Duplication

[klinvill]

@lemmy I rebased this onto the latest changes and think it didn't break anything, but I'd love some extra assurance I didn't break #233

[lemmy]

The work as part of https://github.com/alygin/vscode-tlaplus/issues/242 identified/created the problem that the code can check another specification than what the HTML page shows.