10000 Reform printing of parse error by andreasabel · Pull Request #7437 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Reform printing of parse error #7437

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 4 commits into from
Aug 20, 2024
Merged

Reform printing of parse error #7437

merged 4 commits into from
Aug 20, 2024

Conversation

andreasabel
Copy link
Member
  • use a dedicated ParserError constructor instead of generic Exception
  • print location only once (closes Range printed twice for "Parse error" #7434)
  • prefix with error name
  • only print token context for Happy errors (those that have no explanation)

@andreasabel
Fix #7434: Reform printing of parse error
bbd3fe8 
- use a dedicated `ParserError` constructor instead of generic `Exception`
- print location only once (closes #7434)
- prefix with error name
- only print token context for Happy errors (those that have no explanation)
@andreasabel
Re #7434: update 93 test cases after parse error reform
0ad97e3
@andreasabel andreasabel force-pushed the parse-error branch 2 times, most recently from a078728 to cbbeb30 Compare August 20, 2024 05:44
@andreasabel
Refactor Exception to GenericException String
9b29b3c 
Its `Range` and `Doc` attributes were actually not used.
Renaming to `GenericException` makes it better greppable.
@andreasabel
Make test/api/Makefile more robust
c436dd4
@andreasabel andreasabel added ux: error reporting Issues to do with how Agda reports errors parser Problems with the parser's implementation (rather than with decisions about syntax) labels Aug 20, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Aug 20, 2024
@andreasabel andreasabel added the GenericError Concerning GenericError and GenericDocError label Aug 20, 2024
@andreasabel andreasabel requested a review from UlfNorell August 20, 2024 08:05
UlfNorell
UlfNorell approved these changes Aug 20, 2024
View reviewed changes
Copy link
Member
@UlfNorell UlfNorell left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very nice!

@andreasabel andreasabel merged commit c436dd4 into master Aug 20, 2024
28 checks passed
@andreasabel andreasabel self-assigned this Aug 20, 2024
@andreasabel andreasabel deleted the parse-error branch September 12, 2024 18:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@UlfNorell UlfNorell UlfNorell approved these changes

Assignees

@andreasabel andreasabel

Labels
GenericError Concerning GenericError and GenericDocError parser Problems with the parser's implementation (rather than with decisions about syntax) ux: error reporting Issues to do with how Agda reports errors
Projects
None yet
Milestone
2.8.0
Development

Successfully merging this pull request may close these issues.

Range printed twice for "Parse error"
2 participants
@andreasabel @UlfNorell
0