From 5cfa13d08bc35dddf2fb9c203f45c4587831bc39 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Jul 2019 14:13:50 -0700 Subject: [PATCH] fix(library/init/lean/parser/parser): consume whitespace in the beginning of the input --- library/init/lean/parser/parser.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 60f7bb9b2e..fa5f263be2 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -1074,6 +1074,7 @@ def mkParserState (input : String) : ParserState := def runParser (env : Environment) (tables : ParsingTables) (input : String) (fileName := "") (kind := "
") : 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)