max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/parser/parser): change optional p behavior

Browse source 
It ignores error only if `p` does not consume any input. This change
improves the quality of the error messages. The previous behavior can be
obtained by using `optional (try p)`.
This commit is contained in:
Leonardo de Moura 2019-07-02 07:52:22 -07:00
parent 9d50b3ca47
commit ee2d3faa63
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/parser/parser.lean
View file

@ -276,7 +276,7 @@ instance hashOrelse {k : ParserKind} : HasOrelse (Parser k) :=
let iniSz := s.stackSize;
let iniPos := s.pos;
let s := p a c s;
let s := if s.hasError then s.restore iniSz iniPos else s;
let s := if s.hasError && s.pos == iniPos then s.restore iniSz iniPos else s;
s.mkNode nullKind iniSz
@[inline] def optional {k : ParserKind} (p : Parser k) : Parser k :=