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

fix(library/init/lean/parser/parser): symbolNoWs was not creating an atom

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-08 10:41:40 -07:00
parent 7a89d45391
commit 74c46d2b35
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -974,7 +974,16 @@ def symbolNoWsInfo (sym : String) (lbpNoWs : Option Nat) : ParserInfo :=
@[inline] def symbolNoWsFnAux (sym : String) (errorMsg : String) : ParserFn trailing :=
fun left c s =>
if checkTailNoWs left then
strAux sym errorMsg 0 c s
let startPos := s.pos;
let input := c.input;
let s := strAux sym errorMsg 0 c s;
if s.hasError then s
else
let leading := mkEmptySubstringAt input startPos;
let stopPos := startPos + sym.bsize;
let trailing := mkEmptySubstringAt input stopPos;
let atom := mkAtom { leading := leading, pos := startPos, trailing := trailing } sym;
s.pushSyntax atom
else
s.mkError errorMsg