-
Notifications
You must be signed in to change notification settings - Fork 261
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
Improve reporting of related locations #4929
Improve reporting of related locations #4929
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Creating harmony between error reporting systems brings me happiness. Thanks!
} | ||
|
||
public void WriteSourceCodeSnippet(IToken tok, TextWriter tw) { | ||
string line = GetFileLine(tok.Uri, tok.line - 1); | ||
if (line == null) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Makes sense, thanks for doing that!
yield return SerializeRelated(tok, null, "Related location"); | ||
while (tok is NestedToken nestedToken) { | ||
tok = nestedToken.Inner; | ||
var message = nestedToken.Message != null ? "Related location: " + nestedToken.Message : "Related location"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good job updating this! I don't think it is tested, is it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is, in Source/IntegrationTests/bin/Test/cli/diagnosticsFormats.dfy
rwLock.EnterWriteLock(); | ||
try { | ||
counts[dafnyDiagnostic.Level] = counts.GetValueOrDefault(dafnyDiagnostic.Level, 0) + 1; | ||
if (messageSource != MessageSource.Verifier && messageSource != MessageSource.Compiler) { | ||
if (dafnyDiagnostic.Source != MessageSource.Verifier && dafnyDiagnostic.Source != MessageSource.Compiler) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I like dafnyDiagnostic
more than message
too
|
||
yield return new DafnyRelatedInformation(token, message); | ||
if (inner != null) { | ||
foreach (var nestedInformation in CreateDiagnosticRelatedInformationFor(inner, newMessage)) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One CI warning to fix below
Description
Behavior
Make reporting of related locations more consistent, so related locations are always shown on a separate line. Example:
This style already occurred in many other locations, such as here:
and here:
Refactoring
LocalVariableDeclarationVisitor
into its own file, without changesSymbolDeclarationResolver
into its own file, without changesDiagnosticUtil
into its own file, and rename toDiagnosticsUtil
MapType
into its own file, without changesHow has this been tested?
Expect files have been updated to match the new related location format.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.