From a716528067019e015bdfd5683268fed232518e9b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 13 Apr 2019 08:05:44 -0700 Subject: [PATCH] fix(tests/playground/parser/parser): reset position --- tests/playground/parser/parser.lean | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/tests/playground/parser/parser.lean b/tests/playground/parser/parser.lean index 0d3fbf3dbf..32f27197bd 100644 --- a/tests/playground/parser/parser.lean +++ b/tests/playground/parser/parser.lean @@ -657,13 +657,22 @@ def tokenFn : BasicParserFn def symbolFnAux (sym : String) (errorMsg : String) : BasicParserFn | cfg s d := - let d := tokenFn cfg s d in + let iniPos := d.pos in + let d := tokenFn cfg s d in if d.hasError then + let d := d.setPos iniPos in d.mkError errorMsg else match d.stxStack.back with - | Syntax.atom _ sym' := if sym == sym' then d else d.mkError errorMsg - | _ := d.mkError errorMsg + | Syntax.atom _ sym' := + if sym == sym' then + d + else + let d := d.setPos iniPos in + d.mkError errorMsg + | _ := + let d := d.setPos iniPos in + d.mkError errorMsg @[inline] def symbolFn (sym : String) : BasicParserFn := symbolFnAux sym ("expected '" ++ sym ++ "'")