-
Notifications
You must be signed in to change notification settings - Fork 689
[parser] initialization based on Loc.t rather than Loc.source #9830
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
Conversation
This PR is orthogonal to #9733 but complements the feature it provides. In particular to parse anti quotations and get errors with the right Loc.t, one needs to tell Coq where the text begins. For the reviewers: The old code was storing the file name (Loc.source) in the lexer state and was using it only to generate the initial_loc from which the tokenizing function was starting. I removed this global data, and pass the initial loc to the tokenizing function factory, that grabs it in its closure. No need to have the file name as part of the imperative lexer state anymore. |
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.
This is without a doubt very useful; I think the current interface should play well with the state; even if cLexer
is exposing unfortunately unsafe primitives.
The initial location should be factored to an utility function tho.
I'll let some time for @ppedrot @herbelin to comment, otherwise I'll merge.
391ecc0
to
4016af2
Compare
ping |
We got a conflict, please rebase; will merge this WE. |
In this way one can also set the current offsets in a file, useful if you are parsing a Coq fragment within a file instead of a full file starting from the first line.
done. The conflicts was trivial, I think we could avoid the ping pong between author and assignee in these cases. |
…c.source Reviewed-by: ejgallego Ack-by: gares
In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.