From f5a2562575c0dff769c47d0e8d89fd64392d101e Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 8 Dec 2021 21:37:31 +0100 Subject: [PATCH] fix: indent structure fields --- src/Lean/Parser/Command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index f0fc15f1aa..f4094d06ff 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -81,7 +81,7 @@ def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> def structImplicitBinder := leading_parser atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}" def structInstBinder := leading_parser atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]" def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault) -def structFields := leading_parser manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder)) +def structFields := leading_parser manyIndent (ppLine >> checkColGe >> ppGroup (structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder)) def structCtor := leading_parser atomic (declModifiers true >> ident >> optional inferMod >> " :: ") def structureTk := leading_parser "structure " def classTk := leading_parser "class "