Lean.PrettyPrinter puts comments in invalid places

Prerequisites

[x] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The pretty printer for Command is merging a -- comment line with the following line, causing the result to contain code that is commented out.

Context

[Broader context that the issue occured in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

Run the following:

import Lean
open Lean

-- test `Command`
run_cmd Elab.Command.liftTermElabM do
  let s := "theorem ohno : \n\
    -- commented out:\n\
    1 = 1 := trivial"
  let cmd : Command := ⟨← ofExcept <| Parser.runParserCategory (← getEnv) `command s⟩
  logInfo (← PrettyPrinter.ppCommand cmd)

-- test `Term`
run_cmd Elab.Command.liftTermElabM do
  let s := "∀ x : ℕ,
    -- commented out:\n\
    x = x"
  let cmd : Term := ⟨← ofExcept <| Parser.runParserCategory (← getEnv) `term s⟩
  logInfo (← PrettyPrinter.ppTerm cmd)

Expected behavior: The resulting syntax should be valid

Actual behavior: It is not; it prints out

theorem ohno :
    -- commented out:1 = 1 :=
  trivial

and

∀ x : ℕ,
  -- commented out:x = x

Versions

4.7.0-rc2 (web editor)

Impact

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

leanprover / lean4