From e90bdd00dbb2b000f5bf1a2d9fcec9ea5e5ff5c8 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 8 Dec 2021 21:48:24 +0100 Subject: [PATCH] fix: indent where definitions and add space before --- src/Lean/Parser/Command.lean | 2 +- src/Lean/Parser/Term.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index f4094d06ff..6a13f2ac8e 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -55,7 +55,7 @@ def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithou def declValSimple := leading_parser " :=\n" >> termParser >> optional Term.whereDecls def declValEqns := leading_parser Term.matchAltsWhereDecls def whereStructField := leading_parser Term.letDecl -def whereStructInst := leading_parser "where " >> many1Indent (group (whereStructField >> optional ";")) +def whereStructInst := leading_parser " where" >> many1Indent (ppLine >> ppGroup (group (whereStructField >> optional ";"))) /- Remark: we should not use `Term.whereDecls` at `declVal` because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes. Issue #753 showns an example that fails to be parsed when we used `Term.whereDecls`. diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 9fa00aff7c..8a9c2789fa 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -209,7 +209,7 @@ def letRecDecls := leading_parser sepBy1 letRecDecl ", " def «letrec» := leading_parser:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser @[runBuiltinParserAttributeHooks] -def whereDecls := leading_parser " where" >> many1Indent (ppLine >> group (letRecDecl >> optional ";")) +def whereDecls := leading_parser " where" >> many1Indent (ppLine >> ppGroup (group (letRecDecl >> optional ";"))) @[runBuiltinParserAttributeHooks] def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls