reformat.lean on itself produces code that does not compile

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

• reformat.lean on itself produces broken code

Steps to Reproduce

1. Download https://github.com/leanprover/lean4/blob/master/script/reformat.lean

2. Run the program on the reformat.lean itself

$ lean --run reformat.lean reformat.lean  > out.lean
$ lean --run out.lean out.lean 
out.lean:11:51: error: expected token

$ diff reformat.lean out.lean 
6a7
> 
10c11
<   if cmds.getKind == nullKind || cmds.getKind == ``Parser.Module.header then
---
>   if cmds.getKind == nullKind || cmds.getKind == `` Parser.Module.header then 
30c31
<   for cmd in getCommands cmds |>.run #[] |>.2 do
---
>   for cmd in getCommands cmds |>.run #[] |>.2do
...

Expected behavior: I expected the output of the reformat.lean program to run.

Actual behavior: Error message.

out.lean:11:51: error: expected token

Reproduces how often: 100%

Versions

• Lean (version 4.0.0-nightly-2023-08-11, commit 510bc47cc366, Release)
• Linux anders-MS-7B79 5.15.0-83-generic #92~20.04.1-Ubuntu SMP Mon Aug 21 14:00:49 UTC 2023 x86_64 x86_64 x86_64 GNU/Linux

Additional Information

Zulip comment with suggestion to create this Gitlab issue:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Code.20Formatter/near/388870747

Zulip comment containing smaller example.

Kyle Miller
Here's a minimization:

import Lean

#eval do Lean.PrettyPrinter.ppTerm (← `(``x))
-- `` x✝

Start with script/reformat.lean and reproduce the two commands from the report, then compare the generated out.lean with the listed diff. Use the smaller Lean.PrettyPrinter.ppTerm example to narrow the formatting behavior. Done means running reformat.lean on itself produces output that compiles without the reported token error.