From a8a92d8e8ce0522e9fbd5a5878478d245bafc90a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 15 May 2020 14:40:15 +0200
Subject: [PATCH] feat: parenthesizer: preserve whitespace

---
 src/Init/Lean/PrettyPrinter/Parenthesizer.lean | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/PrettyPrinter/Parenthesizer.lean b/src/Init/Lean/PrettyPrinter/Parenthesizer.lean
index f827d3812f..e540a38665 100644
--- a/src/Init/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Init/Lean/PrettyPrinter/Parenthesizer.lean
@@ -239,10 +239,17 @@ trailRbp' ← if rbp > lbp' || (match trailRbp', lbp with some trailRbp', some l
     -- the original node, we must first move to the right, except if we already were at the left-most child in the first
     -- place.
     when (idx > 0) goRight;
-    setCur (mkParen stx);
+    match stx.getHeadInfo, stx.getTailInfo with
+    | some hi, some ti =>
+      -- Move leading/trailing whitespace of `stx` outside of parentheses
+      let stx := (stx.setHeadInfo { hi with leading := "".toSubstring }).setTailInfo { ti with trailing := "".toSubstring };
+      let stx := mkParen stx;
+      let stx := (stx.setHeadInfo { hi with trailing := "".toSubstring }).setTailInfo { ti with leading := "".toSubstring };
+      setCur stx
+    | _, _ => setCur (mkParen stx);
     goLeft;
     -- after parenthesization, there is no more trailing parser
-    pure none
+    pure (none : Option Nat)
   else pure trailRbp';
 -- If we already had a token at this level (`lbp ≠ none`), keep the trailing parser. Otherwise, use the minimum of
 -- `rbp` and `trailRbp'`.