Goals of tactics often lose line breaks

Hi. I enabled the "allTactics" option to get goals of tactics, and I found that most line breaks ('\n') were missing, with only a few correctly containing "\n".

First I run lake exe repl. My input to REPL is:

{"cmd" :"import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\ntheorem lean_workbook_plus_12679 (f : ℝ → ℝ) (h : ∀ x y z : ℝ, (x + y + z) * f (x * y * z) = 0) : f 0 = 0  := by\n  have h₁ := h 0 0 0\n  simp at h₁\n  have h₂ := h 1 0 0\n  simp at h₂\n  have h₃ := h 0 1 0\n  simp at h₃\n  have h₄ := h 0 0 1\n", "allTactics": true}

And its response is:

{"tactics":
 [{"tactic": "have h₁ := h 0 0 0",
   "proofState": 0,
   "pos": {"line": 9, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 ⊢ f 0 = 0",
   "endPos": {"line": 9, "column": 20}},
  {"tactic": "simp at h₁",
   "proofState": 1,
   "pos": {"line": 10, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : (0 + 0 + 0) * f (0 * 0 * 0) = 0 ⊢ f 0 = 0",
   "endPos": {"line": 10, "column": 12}},
  {"tactic": "have h₂ := h 1 0 0",
   "proofState": 2,
   "pos": {"line": 11, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : True ⊢ f 0 = 0",
   "endPos": {"line": 11, "column": 20}},
  {"tactic": "simp at h₂",
   "proofState": 3,
   "pos": {"line": 12, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : True h₂ : (1 + 0 + 0) * f (1 * 0 * 0) = 0 ⊢ f 0 = 0",
   "endPos": {"line": 12, "column": 12}},
  {"tactic": "have h₃ := h 0 1 0",
   "proofState": 4,
   "pos": {"line": 13, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : True h₂ : f 0 = 0 ⊢ f 0 = 0",
   "endPos": {"line": 13, "column": 20}},
  {"tactic": "simp at h₃",
   "proofState": 5,
   "pos": {"line": 14, "column": 2},
   "goals":
   "f : ℝ → ℝ\nh : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0\nh₁ : True\nh₂ : f 0 = 0\nh₃ : (0 + 1 + 0) * f (0 * 1 * 0) = 0\n⊢ f 0 = 0",
   "endPos": {"line": 14, "column": 12}},
  {"tactic": "have h₄ := h 0 0 1",
   "proofState": 6,
   "pos": {"line": 15, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : True h₂ h₃ : f 0 = 0 ⊢ f 0 = 0",
   "endPos": {"line": 15, "column": 20}}],
 "messages":
 [{"severity": "error",
   "pos": {"line": 8, "column": 110},
   "endPos": {"line": 15, "column": 20},
   "data":
   "unsolved goals\nf : ℝ → ℝ\nh : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0\nh₁ : True\nh₂ h₃ : f 0 = 0\nh₄ : (0 + 0 + 1) * f (0 * 0 * 1) = 0\n⊢ f 0 = 0"}],
 "env": 0}

So only proofState 5 printed '\n' correctly. Could you please fix this problem?

Version of REPL is adbbfcb9d4e61c12db96c45d227de92f21cc17dd, and I tried on v4.9.0-rc1, too.
Version of lean-toolchain is v4.11.0, and I tried on v4.9.0-rc1, too.
Verison of lake is 5.0.0-ec3042d

Reproduce the issue with lake exe repl using the JSON request shown and allTactics: true, then inspect the REPL response handling for goal strings and newline serialization. Done means multiline goals consistently preserve their line breaks in the returned JSON, including the proof states shown in the report.