diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index f84d1d57b89a..da140bdde92d 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -119,28 +119,55 @@ def isInaccessibleUserName : Name → Bool
   | Name.num p _   => isInaccessibleUserName p
   | _              => false
 
-def escapePart (s : String) : Option String :=
-  if s.length > 0 && isIdFirst (s.get 0) && (s.toSubstring.drop 1).all isIdRest then s
+/--
+Creates a round-trippable string name component if possible, otherwise returns `none`.
+Names that are valid identifiers are not escaped, and otherwise, if they do not contain `»`, they are escaped.
+- If `force` is `true`, then even valid identifiers are escaped.
+-/
+def escapePart (s : String) (force : Bool := false) : Option String :=
+  if s.length > 0 && !force && isIdFirst (s.get 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
+variable (sep : String) (escape : Bool) in
+/--
+Uses the separator `sep` (usually `"."`) to combine the components of the `Name` into a string.
+See the documentation for `Name.toString` for an explanation of `escape` and `isToken`.
+-/
+def toStringWithSep (n : Name) (isToken : String → Bool := fun _ => false) : String :=
+  match n with
   | anonymous       => "[anonymous]"
-  | str anonymous s => maybeEscape s
+  | str anonymous s => maybeEscape s (isToken s)
   | num anonymous v => toString v
-  | str n s         => toStringWithSep n ++ sep ++ maybeEscape s
-  | num n v         => toStringWithSep n ++ sep ++ Nat.repr v
+  | str n s         =>
+    -- Escape the last component if the identifier would otherwise be a token
+    let r := toStringWithSep n isToken
+    let r' := r ++ sep ++ maybeEscape s false
+    if escape && isToken r' then r ++ sep ++ maybeEscape s true else r'
+  | num n v         => toStringWithSep n (isToken := fun _ => false) ++ sep ++ Nat.repr v
 where
-  maybeEscape s := if escape then escapePart s |>.getD s else s
+  maybeEscape s force := if escape then escapePart s force |>.getD s else s
 
-protected def toString (n : Name) (escape := true) : String :=
+/--
+Converts a name to a string.
+
+- If `escape` is `true`, then escapes name components using `«` and `»` to ensure that
+  those names that can appear in source files round trip.
+  Names with number components, anonymous names, and names containing `»` might not round trip.
+  Furthermore, "pseudo-syntax" produced by the delaborator, such as `_`, `#0` or `?u`, is not escaped.
+- The optional `isToken` function is used when `escape` is `true` to determine whether more
+  escaping is necessary to avoid parser tokens.
+  The insertion algorithm works so long as parser tokens do not themselves contain `«` or `»`.
+-/
+protected def toString (n : Name) (escape := true) (isToken : String → Bool := fun _ => false) : String :=
   -- never escape "prettified" inaccessible names or macro scopes or pseudo-syntax introduced by the delaborator
-  toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !maybePseudoSyntax) n
+  toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !maybePseudoSyntax) n isToken
 where
   maybePseudoSyntax :=
-    if let .str _ s := n.getRoot then
+    if n == `_ then
+      -- output hole as is
+      true
+    else if let .str _ s := n.getRoot then
       -- could be pseudo-syntax for loose bvar or universe mvar, output as is
       "#".isPrefixOf s || "?".isPrefixOf s
     else
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 0f186bddf61a..9edf59d7bb3e 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -420,7 +420,9 @@ def identNoAntiquot.formatter : Formatter := do
   let stx@(Syntax.ident info _ id _) ← getCur
     | throwError m!"not an ident: {← getCur}"
   let id := id.simpMacroScopes
-  withMaybeTag (getExprPos? stx) (pushToken info id.toString)
+  let tokenTable := getTokenTable (← getEnv)
+  let isToken (s : String) : Bool := (tokenTable.find? s).isSome
+  withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)))
   goLeft
 
 @[combinator_formatter rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do
diff --git a/tests/lean/run/4686.lean b/tests/lean/run/4686.lean
new file mode 100644
index 000000000000..f1a5f7ddb81c
--- /dev/null
+++ b/tests/lean/run/4686.lean
@@ -0,0 +1,53 @@
+import Lean
+/-!
+# Escaping names that are tokens when pretty printing
+-/
+
+
+/-!
+Variable that's a token.
+-/
+section
+variable («forall» : Nat)
+
+/-- info: «forall» + 1 : Nat -/
+#guard_msgs in #check «forall» + 1
+end
+
+
+/-!
+Constant that's a token
+-/
+def «forall» := 1
+
+/-- info: «forall» + 1 : Nat -/
+#guard_msgs in #check «forall» + 1
+
+
+/-!
+Don't escape name components that are tokens if the prefix is not a token.
+-/
+def Exists.forall := 1
+
+/-- info: Exists.forall : Nat -/
+#guard_msgs in #check Exists.forall
+
+
+/-!
+Overly cautious for tokens that are prefixes.
+-/
+def forall.congr := 1
+
+/-- info: «forall».congr : Nat -/
+#guard_msgs in #check forall.congr
+
+
+/-!
+Escape the last name component to avoid a token.
+-/
+notation "Exists.forall" => true
+
+/-- info: Exists.«forall» : Nat -/
+#guard_msgs in #check «Exists».forall
+/-- info: Exists.forall : Bool -/
+#guard_msgs in #check Exists.forall