From 68568e78d3cc6220b8bfb3d3648d003318546d2d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 18 Sep 2020 16:41:32 +0200
Subject: [PATCH] feat: formatter: use hard space after opening structure
 instance brace

---
 src/Lean/Parser/Basic.lean               | 2 ++
 src/Lean/Parser/Term.lean                | 2 +-
 src/Lean/PrettyPrinter/Formatter.lean    | 1 +
 tests/lean/PPRoundtrip.lean.expected.out | 3 +--
 4 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 0a62016483..0dd0bfbb92 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1687,6 +1687,8 @@ withAntiquot (mkAntiquot "fieldIdx" `fieldIdx)
 { fn   := fun c s => s,
   info := epsilonInfo }
 
+/-- No-op parser that advises the pretty printer to emit a non-breaking space. -/
+@[inline] def ppHardSpace : Parser := skip
 /-- No-op parser that advises the pretty printer to emit a space/soft line break. -/
 @[inline] def ppSpace : Parser := skip
 /-- No-op parser that advises the pretty printer to emit a hard line break. -/
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index cca1623f6c..e15d2d541a 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -77,7 +77,7 @@ def sufficesDecl := optIdent >> termParser >> fromTerm
 def structInstArrayRef := parser! "[" >> termParser >>"]"
 def structInstLVal   := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
 def structInstField  := ppGroup $ parser! structInstLVal >> " := " >> termParser
-@[builtinTermParser] def structInst := parser! "{ " >> optional (try (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }"
+@[builtinTermParser] def structInst := parser! "{" >> ppHardSpace >> optional (try (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }"
 def typeSpec := parser! " : " >> termParser
 def optType : Parser := optional typeSpec
 @[builtinTermParser] def subtype := parser! "{ " >> ident >> optType >> " // " >> termParser >> " }"
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 6f565cd2ed..978aeb6087 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -387,6 +387,7 @@ pushLine
 @[combinatorFormatter Lean.Parser.checkOutsideQuot] def checkOutsideQuot.formatter : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.skip] def skip.formatter : Formatter := pure ()
 
+@[combinatorFormatter Lean.Parser.ppHardSpace] def ppHardSpace.formatter : Formatter := 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
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index d0b789e831..24fe7aeda7 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -47,8 +47,7 @@ Type → Type → Type
 1
 42
 "hi"
-{
-  type := Nat,
+{ type := Nat,
   val := 0 :
   PointedType }
 (1, 2, 3)