-
Notifications
You must be signed in to change notification settings - Fork 259
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
Enables output of errorId #4097
Conversation
@@ -218,7 +218,8 @@ public class ConsoleErrorReporter : BatchErrorReporter { | |||
errorLine += $" {msg} {tok.TokenToString(Options)}"; | |||
} | |||
|
|||
if (Options.Verbose && false) { // Need to control tests better before we enable this | |||
if (Options.Verbose) { // Need to control tests better before we enable this | |||
errorLine += "\nID: " + errorId; |
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 think it's a bit confusing to have just "ID:" on a separate line - less obvious that's it's an error id about the previous line. I think this would be clearer:
formatting1-3.dfy(1,0): Warning: File contains no code (ID: ...)
This would probably be even better, to put the id next to "Warning" or "Error", but may require more plumbing:
formatting1-3.dfy(1,0): Warning (ID: ...): File contains no code
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'll put it after the message, so the important part of the message is upfront.
It is still only included when --verbose is on, so it won't affect existsing tests, but will take a bit more sedding to tease it out of the message.
Test/dafny0/formatting1.dfy.expect
Outdated
@@ -23,6 +23,7 @@ module A { | |||
} | |||
} | |||
formatting1-3.dfy(1,0): Warning: File contains no code | |||
ID: |
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'd say we shouldn't print this at all if there is no error code yet.
@@ -1,5 +1,6 @@ | |||
# Reading from symbols.transcript | |||
bank.dfy(4,25): Warning: constructors no longer need 'this' to be listed in modifies clauses | |||
ID: none |
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.
Where is "none" coming from?
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.
Approving knowing that other pending PRs will add tests shortly (since there are now no changes to existing tests, which is good!)
Adds --verbose to parsing and enabling it to emit the errorId and explanation
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.