From eded9530223c755d879d7f461825d7d33fb470e6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 5 Aug 2020 12:23:34 +0200
Subject: [PATCH] feat: formatter: escape identifiers

---
 src/Lean/PrettyPrinter/Formatter.lean | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 8b07988d02..2ba45f5752 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -238,11 +238,20 @@ goLeft
 def identNoAntiquot.formatter : Formatter | _ => do
 checkKind identKind;
 stx ← getCur;
--- TODO: pretty-print Name using «»
-pushToken stx.getId.toString;
+let s := stx.getId.toString;
+-- try to parse `s` as-is; if it fails, escape
+pst ← parseToken s;
+let s := if pst.stxStack == #[stx] then s else match stx.getId with
+  | Name.str Name.anonymous s _ => "«" ++ s ++ "»"
+  | _                           => panic! "unimplemented: escaping non-atomic identifiers (is anyone even using those?)";
+pushToken s;
 goLeft
 
-@[builtinFormatter rawIdent] def rawIdent.formatter := identNoAntiquot.formatter
+@[builtinFormatter rawIdent] def rawIdent.formatter : Formatter | _ => do
+checkKind identKind;
+stx ← getCur;
+pushToken stx.getId.toString;
+goLeft
 
 def visitAtom (k : SyntaxNodeKind) : Formatter | p => do
 stx ← getCur;