Location information in outer lexer #1052
Conversation
This reverts commit d748797.
|
Marking this for review without doing tokens for attributes. Attributes don't have any location information in the kast format, so supporting it would require more work than just getting locations on these tokens. |
| @@ -53,25 +61,33 @@ BUBBLE | |||
| </k> | |||
|
|
|||
| LBRACK | |||
| 1,0 | |||
There was a problem hiding this comment.
This doesn't look right.
There was a problem hiding this comment.
This is one of the attribute tokens, which aren't getting location info because attributes don't have source locations in KAST, so it would be extra work in this PR for nothing. Instead, they're getting the default INIT_LOC.
There was a problem hiding this comment.
It is not for nothing, it enables more fine-grained error reporting for attributes. Please open an issue so that we can address this later.
There was a problem hiding this comment.
In that issue, please also include that we should add the following test.
After lexing, for each token, if we consider the substring of the input text starting at the token location, it will start with the token text.
There was a problem hiding this comment.
|
Converting this to draft to avoid accidentally merging it before the repo merge. |
Transfer of: runtimeverification/pyk#1052 --------- Co-authored-by: Guy Repta <[email protected]>
runtimeverification/k#4180