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

fix(tests/playground/parser/parser): reset position

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-13 08:05:44 -07:00
parent 68e8faeef1
commit a716528067
1 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
tests/playground/parser/parser.lean
View file

@ -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 ++ "'")