From e8ca2e3f6252cc3a56ec67eadcdad0c1c849c374 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 31 Jul 2020 18:24:00 +0200
Subject: [PATCH] feat: formatter: push space at checkWsBefore

---
 src/Lean/PrettyPrinter/Formatter.lean    |  5 ++++-
 tests/lean/PPRoundtrip.lean.expected.out | 14 +++++++-------
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 71240bf952..c6f45b2d7b 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -289,9 +289,12 @@ catch (visit (p.getArg! 0)) $ fun e => match e with
 -- call closure with dummy position
 visit $ mkApp (p.getArg! 0) (mkConst `sorryAx [levelZero])
 
+@[builtinFormatter checkWsBefore] def checkWsBefore.formatter : Formatter | p => do
+modify fun st => { st with leadWord := "" };
+push " "
+
 @[builtinFormatter checkPrec] def checkPrec.formatter : Formatter | p => pure ()
 @[builtinFormatter checkStackTop] def checkStackTop.formatter : Formatter | p => pure ()
-@[builtinFormatter checkWsBefore] def checkWsBefore.formatter : Formatter | p => pure ()
 @[builtinFormatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter | p => pure ()
 @[builtinFormatter checkTailWs] def checkTailWs.formatter : Formatter | p => pure ()
 @[builtinFormatter checkColGe] def checkColGe.formatter : Formatter | p => pure ()
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index 62a9dcbd7d..c3fea5c4bf 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -7,17 +7,17 @@ Type(_+2)
 Nat
 List Nat
 id Nat
-id(id(id Nat))
+id (id (id Nat))
 List Nat
 @id Type Nat
-List.{0}Nat
-id.{2}Nat
-id(@id Type Nat)
+List.{0} Nat
+id.{2} Nat
+id (@id Type Nat)
 λ(a : Nat)=>a
 λ(a b : Nat)=>a
 λ(a : Nat)(b : Bool)=>a
 λ{a b : Nat}=>a
-typeAs({α : Type} → α → α)λ{α : Type}(a : α)=>a
+typeAs ({α : Type} → α → α)λ{α : Type}(a : α)=>a
 λ{α : Type}[_inst_1 : HasToString α](a : α)=>@HasToString.toString α _inst_1 a
 (α : Type) → α
 (α β : Type) → α
@@ -31,5 +31,5 @@ Type → Type → Type
 42
 "hi"
 (Prod.mk 1 2).fst
-or(HasLess.Less 1 2)Bool.true
-id(λ(a : Nat)=>a)0
+or (HasLess.Less 1 2)Bool.true
+id (λ(a : Nat)=>a)0