Open eric-wieser opened 2 months ago
Please put an X between the brackets as you perform the following steps:
While the XML parser correctly handles XML escape sequences, the stringifier does not emit them.
Zulip thread. This leads to some mangled markdown in doc-gen, which unknowingly tries to work around this bug.
Run the following:
import Lean run_cmd do let .ok doc := Lean.Xml.parse "<b class=\""\">hello < world </b>" | unreachable! Lean.logInfo (toString doc)
Expected behavior: The output is <b class=""">hello < world </b>
<b class=""">hello < world </b>
Actual behavior: The output is <b class=""">hello < world </b>, which is invalid XML
<b class=""">hello < world </b>
4.9.0-rc1 4.10.0-nightly-2024-06-09
[Additional information, configuration or data that might be necessary to reproduce the issue]
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.
I'd like to open a PR to fix this. Any suggestions?
Prerequisites
Please put an X between the brackets as you perform the following steps:
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:
Expected behavior: The output is
<b class=""">hello < world </b>
Actual behavior: The output is
<b class=""">hello < world </b>
, which is invalid XMLVersions
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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.