feat: formatter: push space at checkWsBefore

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 ()

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