fix(library/init/lean/parser/module): use updateLeading

2019-08-08 10:45:15 -07:00 · 2019-08-08 10:45:15 -07:00 · 10a8822ac5
commit 10a8822ac5
parent 74c46d2b35
1 changed files with 2 additions and 1 deletions
--- a/library/init/lean/parser/module.lean
+++ b/library/init/lean/parser/module.lean
@ -111,7 +111,8 @@ partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleP
  | (stx, state, msgs) =>
    if isEOI stx then
      if msgs.isEmpty then
-        pure (mkListNode stxs)
+        let stx := mkListNode stxs;
+        pure stx.updateLeading
      else do
        msgs.toList.mfor $ fun msg => IO.println msg;
        throw (IO.userError "failed to parse file")