Add command to run last model check with options #216
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This command works when the model checking pane is selected.
This clarifies the meaning of the argument since if withNewOptions is false, the last options will be used to model check.
|
Kudos, SonarCloud Quality Gate passed!
|
|
Closing in favor of #222 due to the preference here: #215 (comment) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Addresses #215.
This PR adds a command ("Run last model check with new options") that works when the model checking pane is focused.
Alternative implementations could include adding a link to the model checking webview that runs this command, or updating the
tlaplus.model.check.runcommand to also be enabled when the model checking pane is focused. Unfortunately I wasn't able to find a good way to enable the command if a webview is selected that doesn't involve manually setting the context so I instead opted for a new command that re-uses existing functions.