feat: unicodeSymbol.formatter: prefer symbol used in syntax tree

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;

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