-
Notifications
You must be signed in to change notification settings - Fork 350
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
Preserve token parse errors #347
Conversation
if s.hasError then | ||
-- Discard token parse errors and break the trailing loop instead. | ||
-- The error will be flagged when the next leading position is parsed, unless the token | ||
-- is in fact valid there (e.g. EOI at command level, no-longer forbidden token) | ||
return s.restore iniSz iniPos |
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.
@leodemoura This was the critical condition that took me a while to figure out
@@ -11,7 +11,7 @@ namespace Parser | |||
|
|||
namespace Command | |||
def commentBody : Parser := | |||
{ fn := rawFn (finishCommentBlock 1) true } | |||
{ fn := rawFn (fun c s => finishCommentBlock s.pos 1 c s) (trailingWs := true) } |
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.
Not exactly the start position of the comment, but close enough
else | ||
let curr := input.get i | ||
let s := s.setPos (input.next i) | ||
if curr == '\"' then | ||
let s := mkNodeToken interpolatedStrLitKind startPos c s | ||
s.mkNode interpolatedStrKind stackSize | ||
else if curr == '\\' then | ||
let s := s.next c.input i |
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.
@leodemoura I have no idea how this was working until now :)
…er#347) Now that leanprover@cdb855d has landed, `initialize` statements can get real docstrings, and we no longer need to silence the linter.
No description provided.