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

fix(library/init/lean/parser/parser): consume whitespace in the beginning of the input

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-08 14:13:50 -07:00
parent f66f6fd455
commit 5cfa13d08b
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1074,6 +1074,7 @@ def mkParserState (input : String) : ParserState :=
def runParser (env : Environment) (tables : ParsingTables) (input : String) (fileName := "<input>") (kind := "<main>") : Except String Syntax :=
let c := mkParserContext env input fileName;
let s := mkParserState input;
let s := whitespace c s;
let s := prattParser kind tables (0 : Nat) c s;
if s.hasError then
Except.error (s.toErrorMsg c)