Skip to content
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

Resolution errors do not get migrated / do not disappear when there are parse errors #5428

Closed
MikaelMayer opened this issue May 10, 2024 · 0 comments · Fixed by #5429
Closed

Comments

@MikaelMayer
Copy link
Member

image

How to reproduce

Parse the following code:

module ResolutionError {
  import   UnderlineComments2
}

Then, place the caret just before the "m" of module and then paste the following code (including the final newline)

module ParseError {
  // I can underline comments in red.

  function method Test() {

  }
}

The problem is, resolution errors are not migrated, and second, resolution errors should be marked as obsolete if parse error occur, just in case, so that users know to focus on parse error instead of resolution errors. Or resolution error should disappear if parse errors occur. But I think that if we could do the same that we do for verification, leave them there

@keyboardDrummer keyboardDrummer transferred this issue from dafny-lang/ide-vscode May 13, 2024
keyboardDrummer added a commit that referenced this issue May 14, 2024
Fixes #5428

### Description
- Revert part of #5243 because
this caused complication and it needs better consideration before being
done.

### How has this been tested?
- Added `ResolutionErrorMigration` to verify
#5428 is fixed
- Update `CorrectParseDiagnosticsDoNotOverridePreviousResolutionOnes` to
account for resolution diagnostics no longer being migrated

<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
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant