Identifier pretty-printing can clash with notation

[eric-wieser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Identifiers that clash with syntax are not escaped when pretty-printing. As a result, the content of the goal view cannot be pasted into the source file.

Context

Zulip thread

Steps to Reproduce

1. Run the following:

variable («forall» : Nat)

#check «forall» + 1 -- forall + 1 : Nat

-- paste what we got from the goal view
#check forall + 1 -- syntax error

Expected behavior: The output of the first #check should rountrip; probably, it should be «forall» + 1 : Nat.

Actual behavior: The escaping of forall is lost, resulting in a syntax error. set_option pp.all true does not help.

Versions

4.10.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.