From 9b6370bdbe3e746605d62b39de13daec416bc560 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 17 Sep 2020 16:29:47 +0200
Subject: [PATCH] feat: formatter: escaping compound identifiers

---
 src/Lean/PrettyPrinter/Formatter.lean | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 2d3fcea7fe..4f6364acef 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -272,10 +272,13 @@ else if id.components.any Name.isNum then
 else do {
   -- 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
+  if pst.stxStack == #[stx] then
+    pushToken s
+  else
+    let n := stx.getId;
+    -- TODO: do something better than escaping all parts
+    let n := (n.components.map fun c => "«" ++ toString c ++ "»").foldl mkNameStr Name.anonymous;
+    pushToken n.toString
 };
 goLeft