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

Errors should have multiple locations, not just one #998

Open
cpitclaudel opened this issue Apr 19, 2017 · 0 comments
Open

Errors should have multiple locations, not just one #998

cpitclaudel opened this issue Apr 19, 2017 · 0 comments

Comments

@cpitclaudel
Copy link
Contributor

cpitclaudel commented Apr 19, 2017

This should be an easy change, though it touches a bunch of places in the code. The idea is that some errors come with multiple ranges, and these should all be reported to the user. The interactive mode already accepts lists of ranges, so no changes would be needed on that side.

Currently, F* reports auxiliary locations as strings ("see also …", "Also see …"). It would be much nicer to return these locations as lists of ranges.

This was brought up by @fournet, who noted that being able to jump between errors and related locations would be convenient.

cpitclaudel added a commit to FStarLang/fstar-mode.el that referenced this issue Apr 20, 2017
This should be fixed on the F* side, but it's easy to do it here while waiting
for FStarLang/FStar#998
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant