From 4eb270a572d1ebed37e62d774b131e2c56545ef4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 31 Mar 2015 15:07:32 -0700
Subject: [PATCH] fix(frontends/lean/pp): extra space

---
 src/frontends/lean/pp.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index e17460fbb..9a598318a 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1040,7 +1040,8 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
                     curr = curr + space();
                 fmt = curr + fmt;
             }
-            extra_space = add_extra_space(tk);
+            if (m_extra_spaces || !last_is_skip)
+                extra_space = add_extra_space(tk);
         }
         unsigned first_lbp = inf_bp();
         if (!entry.is_nud()) {