Closed acmepjz closed 2 months ago
Example of the changes of Init/Conv.html
:
line 27: in "head position" until a constructor is exposed. ...
line 31: ... Performs one step of "congruence", which takes a term and produces
line 92: ... closes one conv goal "trivially", by using reflexivity
line 146: by focusing on particular subexpressions.</p><p>See <https://lean-lang.org/theorem_proving_in_lean4/conv.html> for more details. ...
line 27: in "head position" until a constructor is exposed. ...
line 31: ... Performs one step of "congruence", which takes a term and produces
line 92: ... closes one conv goal "trivially", by using reflexivity
line 146: by focusing on particular subexpressions.</p><p>See <a href="https://lean-lang.org/theorem_proving_in_lean4/conv.html">https://lean-lang.org/theorem_proving_in_lean4/conv.html</a> for more details. ...
As you can see, the <url>
in original line 146 is completely broken (https://leanprover-community.github.io/mathlib4_docs/Init/Conv.html#Lean.Parser.Tactic.Conv.conv), while this PR fixes it. This PR also introduces changes that "
is replaced by "
, similarly for <
, >
and &
, but these changes in HTML text does not affect rendering.
Need to ensure that #126 does not reappear.
have a reference to the upstream issue in the source
Done.
Looks fine to me, let's see if some users find pages that are broken again^^
This PR fixes
<url>
processing problem of markdown introduced by #157. It turns out that the problem occurred atLean.Xml.instToStringElement
which does not do escape. The code is copied fromLean.Xml.instToStringElement
with escape code added. The added functions should be removed once https://github.com/leanprover/lean4/issues/4411 is fixed.discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Contribution.20to.20doc-gen4.3F/near/443537944