fix: apply newlines before and after comments when formatting syntax

[kmill]

This PR closes #3791, making sure that the Syntax formatter inserts whitespace before and after comments in the leading and trailing text of Syntax to avoid having comments comment out any following syntax, and to avoid comments' lexical syntax from being interpreted as being part of another syntax. If the text contains newlines before or after any comments, they are formatted as hard newlines rather than soft newlines. For example, -- comments will have a hard newline after them. Note: metaprograms generating Syntax with comments should be sure to include newlines at the ends of -- comments.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-13 08:55:14)
  Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-06-13 18:40:40)