From 82078fba84c868040bdfb4e27f1757f27dde6217 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 7 Jan 2020 14:29:31 -0500
Subject: [PATCH] chore: make Syntax.reprint output without source info more
 readable

---
 src/Init/Lean/Syntax.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index 6d54e7847c..55ab07b8b6 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -284,7 +284,11 @@ match setTailInfoAux info stx with
 | none     => stx
 
 private def reprintLeaf : Option SourceInfo → String → String
-| none,      val => val
+-- no source info => add gracious amounts of whitespace to definitely separate tokens
+-- Note that the proper pretty printer does not use this function.
+-- The parser as well always produces source info, so round-tripping is still
+-- guaranteed.
+| none,      val => " " ++ val ++ " "
 | some info, val => info.leading.toString ++ val ++ info.trailing.toString
 
 partial def reprint : Syntax → Option String