dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.82k stars 253 forks source link

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

Closed MikaelMayer closed 2 weeks ago

MikaelMayer commented 3 weeks ago

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