-
Notifications
You must be signed in to change notification settings - Fork 271
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Using {:only}
to focus verification
#4432
Labels
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
release-blocker
Must be resolved before the next release
Comments
MikaelMayer
added a commit
that referenced
this issue
Sep 19, 2023
…displayed as verified in the gutter icons (#4433) This PR fixes #4432 I added the corresponding test. Because the Skipped gutter icon is not supported yet in VSCode, it's just rendered as no icon, which is suitable for now at least to indicate that a method is not verified. | Before, without this PR | With this PR | |--------------------------|---------------| |  |  | |--------------------------|--------------| |  |  | |--------------------------|--------------| <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer
pushed a commit
that referenced
this issue
Sep 26, 2023
…displayed as verified in the gutter icons (#4433) This PR fixes #4432 I added the corresponding test. Because the Skipped gutter icon is not supported yet in VSCode, it's just rendered as no icon, which is suitable for now at least to indicate that a method is not verified. | Before, without this PR | With this PR | |--------------------------|---------------| |  |  | |--------------------------|--------------| |  |  | |--------------------------|--------------| <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
part: language server
Support for LSP in Dafny (server part; client is in ide-vscode repo)
release-blocker
Must be resolved before the next release
This is a great feature.
However, everything that is not
{:only}
will also be tagged green.They really should be grey/or black.
Since they are not verified.
Also, there should be a color for things changed outside
{:only}
.Take the following situation.
I am working on
method A
and have tagged it{:only}
so that I can focus my verification.
I realize that
function B
is involved.If I add an extra
ensures
tofunction B
then I can make progress on
method A
.However, since I have only marked
method A
{:only}
this change is not verified.
Ideally the IDE should either mark
function B
{:only}
or update the gutter so that it is clear that this is not verified...
Update by @MikaelMayer:
The text was updated successfully, but these errors were encountered: