From 74c46d2b354c19102d9ea6d150d9797c599071e9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Aug 2019 10:41:40 -0700 Subject: [PATCH] fix(library/init/lean/parser/parser): `symbolNoWs` was not creating an atom --- library/init/lean/parser/parser.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index c1eb473d45..95926fea4f 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -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