diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index bc69d52b1e..0a62016483 100644 --- a/src/Lean/Parser/Basic.lean +++ b/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 diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 2e941dea8f..cca1623f6c 100644 --- a/src/Lean/Parser/Term.lean +++ b/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 /- diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 6438a0c20b..7413cdb6b7 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/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 diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index 4e2ea8a9de..89428e4839 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/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