ToString instance for Xml does not correctly escape

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

While the XML parser correctly handles XML escape sequences, the stringifier does not emit them.

Context

Zulip thread. This leads to some mangled markdown in doc-gen, which unknowingly tries to work around this bug.

Steps to Reproduce

Run the following:

import Lean

run_cmd do
  let .ok doc := Lean.Xml.parse "<b class=\"&quot;\">hello &lt; world </b>" | unreachable!
  Lean.logInfo (toString doc)

Expected behavior: The output is <b class="&quot;">hello &lt; world </b>

Actual behavior: The output is <b class=""">hello < world </b>, which is invalid XML

Versions

4.9.0-rc1
4.10.0-nightly-2024-06-09

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

Start by running the supplied Lean.Xml.parse and toString reproduction, then locate the Lean.Xml stringifier and compare it with the parser's escape handling. Done means toString emits valid XML with quotes and angle brackets escaped as shown in the expected output, without breaking the reported doc-gen use case.