Copy/pasting goal in Infoview collapses spacing between hypothesis names

[kmill]

Description

Copy/pasting the goal state from the Infoview is useful when making examples, to document what the goal state is supposed to be. However, with the way the goal state is being rendered, there is no space between local hypothesis names or between a local hypothesis name and the :.

Steps to Reproduce

Take for example

example (P Q : Nat → Int → Prop) : ∀ x y, P x y ↔ Q x y := by
  intro x y
  sorry

and move your cursor at the start of sorry.

This is the goal in the Infoview:

Select all the text:

Copy it (with Cmd-C in my case) and then paste it somewhere.

Expected behavior: You get

P Q : ℕ → ℤ → Prop
x : ℕ
y : ℤ
⊢ P x y ↔ Q x y

Actual behavior: You get

PQ: ℕ → ℤ → Prop
x: ℕ
y: ℤ
⊢ P x y ↔ Q x y

Versions

Version of vscode-lean4: v0.0.128

#eval Lean.versionString -- "4.6.0-rc1"

OS: macOS 14.1.1 on M2

Impact

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

[kmill]

If I understand it correctly, the issue is from the fact that the spacing is created using the mr1 style here rather than by perhaps adding   here like how it's added after the colon.