From ea266e48ab85e355a4d83aaddb1addd4aa9a7e95 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 20 Aug 2020 18:57:08 +0200
Subject: [PATCH] feat: unicodeSymbol.formatter: prefer symbol used in syntax
 tree

---
 src/Lean/PrettyPrinter/Formatter.lean    | 12 +++++++++++-
 tests/lean/PPRoundtrip.lean.expected.out | 14 +++++++-------
 2 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 06eff4e96c..5667d05df9 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -278,9 +278,19 @@ pushToken sym;
 goLeft
 
 @[combinatorFormatter symbolNoWs] def symbolNoWs.formatter := symbol.formatter
-@[combinatorFormatter unicodeSymbol] def unicodeSymbol.formatter := symbol.formatter
 @[combinatorFormatter nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter
 
+@[combinatorFormatter unicodeSymbol]
+def unicodeSymbol.formatter (sym asciiSym : String) : Formatter := do
+stx ← getCur;
+Syntax.atom _ val ← pure stx
+  | throw $ Exception.other Syntax.missing $ "not an atom: " ++ toString stx;
+if val == sym.trim then
+  pushToken sym
+else
+  pushToken asciiSym;
+goLeft
+
 @[combinatorFormatter identNoAntiquot]
 def identNoAntiquot.formatter : Formatter := do
 checkKind identKind;
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index 4d7ef4e423..0209677c40 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -13,12 +13,12 @@ List 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
-λ {α : Type}[_inst_1 : HasToString α](a : α) => @HasToString.toString α _inst_1 a
+fun (a : Nat) => a
+fun (a b : Nat) => a
+fun (a : Nat)(b : Bool) => a
+fun {a b : Nat} => a
+typeAs ({α : Type} → α → α) fun {α : Type}(a : α) => a
+fun {α : Type}[_inst_1 : HasToString α](a : α) => @HasToString.toString α _inst_1 a
 (α : Type) → α
 (α β : Type) → α
 Type → Type → Type
@@ -32,4 +32,4 @@ Type → Type → Type
 "hi"
 (Prod.mk 1 2).fst
 or (HasLess.Less 1 2) Bool.true
-id (λ (a : Nat) => a) 0
+id (fun (a : Nat) => a) 0