fix: pp internal names

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)

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