From 650e836ab3e31693e094651ed1f59ea45d1576a0 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Sep 2020 13:34:11 +0200
Subject: [PATCH] fix: pp internal names

---
 src/Lean/Data/Name.lean               |  8 ++++++++
 src/Lean/PrettyPrinter/Formatter.lean | 22 +++++++++++++++-------
 2 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index ce82a3001e..d84f4c8a0f 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -130,6 +130,14 @@ def isAnonymous : Name → Bool
 | anonymous         => true
 | _                 => false
 
+def isStr : Name → Bool
+| str _ _ _ => true
+| _         => false
+
+def isNum : Name → Bool
+| num _ _ _ => true
+| _         => false
+
 end Name
 
 open Std (RBMap RBTree mkRBMap mkRBTree)
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 9f125eaab7..d0998e2c47 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -308,13 +308,21 @@ goLeft
 def identNoAntiquot.formatter : Formatter := do
 checkKind identKind;
 stx ← getCur;
-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;
+let id := stx.getId;
+let s := id.toString;
+if id.isAnonymous then
+  pushToken "[anonymous]"
+else if id.components.any Name.isNum then
+  -- not parsable anyway, output as-is
+  pushToken s
+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
+};
 goLeft
 
 @[combinatorFormatter rawIdent] def rawIdent.formatter : Formatter := do