From ee2d3faa6369b8a977c81153cea8ca470a252ff7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Jul 2019 07:52:22 -0700 Subject: [PATCH] feat(library/init/lean/parser/parser): change `optional p` behavior 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)`. --- library/init/lean/parser/parser.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index d10d950f71..6b08875ec0 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -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 :=