diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index bad7c7f976..931227bf99 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -69,15 +69,45 @@ def isIdEndEscape (c : Char) : Bool := c = idEndEscape
 
 namespace Name
 
-def toStringWithSep (sep : String) : Name → String
-  | anonymous         => "[anonymous]"
-  | str anonymous s _ => s
-  | num anonymous v _ => toString v
-  | str n s _         => toStringWithSep sep n ++ sep ++ s
-  | num n v _         => toStringWithSep sep n ++ sep ++ Nat.repr v
+def getRoot : Name → Name
+  | anonymous             => anonymous
+  | n@(str anonymous _ _) => n
+  | n@(num anonymous _ _) => n
+  | str n _ _             => getRoot n
+  | num n _ _             => getRoot n
 
-protected def toString : Name → String :=
-  toStringWithSep "."
+@[export lean_is_inaccessible_user_name]
+def isInaccessibleUserName : Name → Bool
+  | Name.str _ s _   => s.contains '✝' || s == "_inaccessible"
+  | Name.num p idx _ => isInaccessibleUserName p
+  | _                => false
+
+def escapePart (s : String) : Option String :=
+  if s.length > 0 && isIdFirst s[0] && (s.toSubstring.drop 1).all isIdRest then s
+  else if s.any isIdEndEscape then none
+  else some <| idBeginEscape.toString ++ s ++ idEndEscape.toString
+
+-- NOTE: does not roundtrip even with `escape = true` if name is anonymous or contains numeric part or `idEndEscape`
+variable (sep : String) (escape : Bool)
+def toStringWithSep : Name → String
+  | anonymous         => "[anonymous]"
+  | str anonymous s _ => maybeEscape s
+  | num anonymous v _ => toString v
+  | str n s _         => toStringWithSep n ++ sep ++ maybeEscape s
+  | num n v _         => toStringWithSep n ++ sep ++ Nat.repr v
+where
+  maybeEscape s := if escape then escapePart s |>.getD s else s
+
+protected def toString (n : Name) (escape := true) : String :=
+  -- never escape "prettified" inaccessible names or macro scopes or pseudo-syntax introduced by the delaborator
+  toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !maybePseudoSyntax) n
+where
+  maybePseudoSyntax :=
+    if let Name.str _ s _ := n.getRoot then
+      -- could be pseudo-syntax for loose bvar or universe mvar, output as is
+      "#".isPrefixOf s || "?".isPrefixOf s
+    else
+      false
 
 instance : ToString Name where
   toString n := n.toString
@@ -369,6 +399,9 @@ def mkNumLit (val : String) (info := SourceInfo.none) : Syntax :=
 def mkScientificLit (val : String) (info := SourceInfo.none) : Syntax :=
   mkLit scientificLitKind val info
 
+def mkNameLit (val : String) (info := SourceInfo.none) : Syntax :=
+  mkLit nameLitKind val info
+
 /- Recall that we don't have special Syntax constructors for storing numeric and string atoms.
    The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or
    different ways of representing them. So, our atoms contain just the parsed string.
@@ -665,12 +698,23 @@ instance : Quote String := ⟨Syntax.mkStrLit⟩
 instance : Quote Nat := ⟨fun n => Syntax.mkNumLit <| toString n⟩
 instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[quote s.toString]⟩
 
-private def quoteName : Name → Syntax
-  | Name.anonymous => mkCIdent ``Name.anonymous
-  | Name.str n s _ => Syntax.mkCApp ``Name.mkStr #[quoteName n, quote s]
-  | Name.num n i _ => Syntax.mkCApp ``Name.mkNum #[quoteName n, quote i]
+-- in contrast to `Name.toString`, we can, and want to be, precise here
+private def getEscapedNameParts? (acc : List String) : Name → OptionM (List String)
+  | Name.anonymous => acc
+  | Name.str n s _ => do
+    let s ← Name.escapePart s
+    getEscapedNameParts? (s::acc) n
+  | Name.num n i _ => none
 
-instance : Quote Name := ⟨quoteName⟩
+private def quoteNameMk : Name → Syntax
+  | Name.anonymous => mkCIdent ``Name.anonymous
+  | Name.str n s _ => Syntax.mkCApp ``Name.mkStr #[quoteNameMk n, quote s]
+  | Name.num n i _ => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i]
+
+instance : Quote Name where
+  quote n := match getEscapedNameParts? [] n with
+    | some ss => mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ ".".intercalate ss)]
+    | none    => quoteNameMk n
 
 instance {α β : Type} [Quote α] [Quote β] : Quote (α × β) where
   quote
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 4f80d525bc..92334a9d56 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -20,13 +20,6 @@ def getPrefix : Name → Name
   | str p s _ => p
   | num p s _ => p
 
-def getRoot : Name → Name
-  | anonymous             => anonymous
-  | n@(str anonymous _ _) => n
-  | n@(num anonymous _ _) => n
-  | str n _ _             => getRoot n
-  | num n _ _             => getRoot n
-
 def getString! : Name → String
   | str _ s _ => s
   | _         => unreachable!
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
index e526295cec..97c2d835a4 100644
--- a/src/Lean/Hygiene.lean
+++ b/src/Lean/Hygiene.lean
@@ -62,12 +62,6 @@ private def mkInaccessibleUserName (unicode : Bool) : Name → Name
       Name.mkNum (mkInaccessibleUserName unicode p) idx
   | n => n
 
-@[export lean_is_inaccessible_user_name]
-def isInaccessibleUserName : Name → Bool
-  | Name.str _ s _   => s.contains '✝' || s == "_inaccessible"
-  | Name.num p idx _ => isInaccessibleUserName p
-  | _                => false
-
 def sanitizeNamesDefault := true
 def getSanitizeNames (o : Options) : Bool:= o.get `pp.sanitizeNames sanitizeNamesDefault
 builtin_initialize
diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index 4615e50841..9df31bfbe7 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import Lean.Hygiene
 import Lean.Meta.InferType
 
 namespace Lean.Meta
@@ -132,7 +131,7 @@ def collect (goalTarget : Expr) : MetaM (NameSet × NameSet) := do
   else
     let lctx ← getLCtx
     let hiddenInaccessible := lctx.foldl (init := {}) fun hiddenInaccessible localDecl => do
-      if isInaccessibleUserName localDecl.userName then
+      if localDecl.userName.isInaccessibleUserName then
         hiddenInaccessible.insert localDecl.fvarId
       else
         hiddenInaccessible
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index b6ff2b5819..c149fcb012 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1054,9 +1054,9 @@ private def nameLitAux (startPos : Nat) : ParserFn := fun c s =>
   else
     let stx := s.stxStack.back
     match stx with
-    | Syntax.ident _ rawStr _ _ =>
+    | Syntax.ident info rawStr _ _ =>
       let s := s.popSyntax
-      s.pushSyntax (Syntax.node nameLitKind #[mkAtomFrom stx rawStr.toString])
+      s.pushSyntax (Syntax.mkNameLit rawStr.toString info)
     | _ => s.mkError "invalid Name literal"
 
 private def tokenFnAux : ParserFn := fun c s =>
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 00c4837ad3..a15741c694 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -336,27 +336,11 @@ def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do
 
 @[combinatorFormatter Lean.Parser.identNoAntiquot]
 def identNoAntiquot.formatter : Formatter := do
-  checkKind identKind;
+  checkKind identKind
   let Syntax.ident info _ id _ ← getCur
     | throwError m!"not an ident: {← getCur}"
   let id := id.simpMacroScopes
-  let s := id.toString;
-  if id.isAnonymous then
-    pushToken info "[anonymous]"
-  else if isInaccessibleUserName id || id.components.any Name.isNum ||
-    -- loose bvar
-    "#".isPrefixOf s then
-    -- not parsable anyway, output as-is
-    pushToken info s
-  else
-    -- try to parse `s` as-is; if it fails, escape
-    let pst ← parseToken s
-    if pst.pos == s.bsize then
-      pushToken info s
-    else
-      -- TODO: do something better than escaping all parts
-      let id := (id.components.map fun c => "«" ++ toString c ++ "»").foldl Name.mkStr Name.anonymous
-      pushToken info id.toString
+  pushToken info id.toString
   goLeft
 
 @[combinatorFormatter Lean.Parser.rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do
diff --git a/tests/lean/301.lean.expected.out b/tests/lean/301.lean.expected.out
index 7c936244a8..8fc4ec4b44 100644
--- a/tests/lean/301.lean.expected.out
+++ b/tests/lean/301.lean.expected.out
@@ -1,8 +1,8 @@
 301.lean:1:9-1:17: error: missing cases:
 (Nat.succ _)
 301.lean:1:21-1:24: error: type mismatch
-  
-    (
+  «»
+    («»
       fun (x : Nat) =>
         match x with 
         | 0 => 0)
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 9fc3dcb4db..a303f4dbcc 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -3,9 +3,9 @@ StxQuot.lean:8:12: error: expected command, identifier or term
 "<missing>"
 "<missing>"
 "<missing>"
-"(term_+_ <missing> \"+\" (numLit \"1\"))"
-"(term_+_ <missing> \"+\" (numLit \"1\"))"
-"(term_+_ (numLit \"1\") \"+\" (numLit \"1\"))"
+"(«term_+_» <missing> \"+\" (numLit \"1\"))"
+"(«term_+_» <missing> \"+\" (numLit \"1\"))"
+"(«term_+_» (numLit \"1\") \"+\" (numLit \"1\"))"
 StxQuot.lean:18:15: error: expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] \"=>\" `a._@.UnhygienicMain._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])))"
@@ -13,11 +13,11 @@ StxQuot.lean:18:15: error: expected term
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
-"(term_$__\n `f._@.UnhygienicMain._hyg.1\n \"$\"\n (Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 (numLit \"1\")]))"
+"(«term_$__»\n `f._@.UnhygienicMain._hyg.1\n \"$\"\n (Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 (numLit \"1\")]))"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1])"
 "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
-"(term_+_ (numLit \"2\") \"+\" (numLit \"1\"))"
-"(term_+_ (term_+_ (numLit \"1\") \"+\" (numLit \"2\")) \"+\" (numLit \"1\"))"
+"(«term_+_» (numLit \"2\") \"+\" (numLit \"1\"))"
+"(«term_+_» («term_+_» (numLit \"1\") \"+\" (numLit \"2\")) \"+\" (numLit \"1\"))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\") [])))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\") [])))]"
 "0"
@@ -36,8 +36,8 @@ StxQuot.lean:18:15: error: expected term
 "(Term.structInst\n \"{\"\n []\n [(group\n   (Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)\n   [])]\n (Term.optEllipsis [])\n []\n \"}\")"
 "(Command.section \"section\" [])"
 "(Command.section \"section\" [`foo._@.UnhygienicMain._hyg.1])"
-"(Term.match\n \"match\"\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n    \"=>\"\n    (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
-"(Term.match\n \"match\"\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n    \"=>\"\n    (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
+"(Term.match\n \"match\"\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n    \"=>\"\n    («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
+"(Term.match\n \"match\"\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n    \"=>\"\n    («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
 "#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]"
 "1"
 "(Term.sufficesDecl [] `x._@.UnhygienicMain._hyg.1 (Term.fromTerm \"from\" `x._@.UnhygienicMain._hyg.1))"