From 519eda24596e71eea120fac856a5e39a5d5dc6ee Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 18 Sep 2020 16:36:43 +0200
Subject: [PATCH] feat: formatter: interpret checkWsBefore as soft space

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

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 7413cdb6b7..6f565cd2ed 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -375,7 +375,7 @@ p
 
 @[combinatorFormatter checkWsBefore] def checkWsBefore.formatter : Formatter := do
 modify fun st => { st with leadWord := "" };
-push " "
+pushLine
 
 @[combinatorFormatter checkPrec] def checkPrec.formatter : Formatter := pure ()
 @[combinatorFormatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index 89428e4839..d0b789e831 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -20,7 +20,9 @@ fun
   (b : Bool) =>
   a
 fun {a b : Nat} => a
-typeAs ({α : Type} → α → α) fun
+typeAs
+  ({α : Type} → α → α)
+  fun
     {α : Type}
     (a : α) =>
     a
@@ -52,6 +54,6 @@ Type → Type → Type
 (1, 2, 3)
 (1, 2).fst
 1 < 2 || true
-id (fun
-      (a : Nat) =>
-      a) 0
+id
+  (fun (a : Nat) => a)
+  0