feat: formatter: group+indent binders and structure instance fields

src/Lean/Parser/Basic.lean

@@ -1691,6 +1691,10 @@ withAntiquot (mkAntiquot "fieldIdx" `fieldIdx)
 @[inline] def ppSpace : Parser := skip
 /-- No-op parser that advises the pretty printer to emit a hard line break. -/
 @[inline] def ppLine : Parser := skip
+/--
+  No-op parser combinator that advises the pretty printer to group and indent the given syntax.
+  By default, only syntax categories are grouped. -/
+@[inline] def ppGroup : Parser → Parser := id
 
 end Parser
 

src/Lean/Parser/Term.lean

@@ -76,7 +76,7 @@ def sufficesDecl := optIdent >> termParser >> fromTerm
 @[builtinTermParser] def «show»     := parser!:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
 def structInstArrayRef := parser! "[" >> termParser >>"]"
 def structInstLVal   := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
-def structInstField  := parser! structInstLVal >> " := " >> termParser
+def structInstField  := ppGroup $ parser! structInstLVal >> " := " >> termParser
 @[builtinTermParser] def structInst := parser! "{ " >> optional (try (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }"
 def typeSpec := parser! " : " >> termParser
 def optType : Parser := optional typeSpec
@@ -89,9 +89,9 @@ def binderIdent : Parser  := ident <|> hole
 def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
 def binderTactic  := parser! try (" := " >> " by ") >> Tactic.indentedNonEmptySeq
 def binderDefault := parser! " := " >> termParser
-def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
-def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
-def instBinder := parser! "[" >> optIdent >> termParser >> "]"
+def explicitBinder (requireType := false) := ppGroup $ parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
+def implicitBinder (requireType := false) := ppGroup $ parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
+def instBinder := ppGroup $ parser! "[" >> optIdent >> termParser >> "]"
 def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
 
 /-

src/Lean/PrettyPrinter/Formatter.lean

@@ -389,6 +389,7 @@ push " "
 
 @[combinatorFormatter Lean.Parser.ppSpace] def ppSpace.formatter : Formatter := pushLine
 @[combinatorFormatter Lean.Parser.ppLine] def ppLine.formatter : Formatter := push "\n"
+@[combinatorFormatter Lean.Parser.ppGroup] def ppGroup.formatter (p : Formatter) : Formatter := p *> indentTop *> groupTop
 
 @[combinatorFormatter pushNone] def pushNone.formatter : Formatter := goLeft
 

tests/lean/PPRoundtrip.lean.expected.out

@@ -21,39 +21,33 @@ fun
   a
 fun {a b : Nat} => a
 typeAs ({α : Type} → α → α) fun
-    {α :
-    Type}
+    {α : Type}
     (a : α) =>
     a
 fun
-  {α :
-  Type}
+  {α : Type}
   [inst :
-  HasToString α]
+    HasToString α]
   (a : α) =>
   @toString α inst a
 (α : Type) → α
 (α β : Type) → α
 Type → Type → Type
 (α : Type) → α → α
-(α :
-  Type) →
+(α : Type) →
   (a : α) → a = a
 {α : Type} → α
-{α :
-  Type} →
+{α : Type} →
   [inst :
-    HasToString α] →
+      HasToString α] →
     α
 0
 1
 42
 "hi"
 {
-  type :=
-  Nat,
-  val :=
-  0 :
+  type := Nat,
+  val := 0 :
   PointedType }
 (1, 2, 3)
 (1, 2).fst