search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 9 forks source link

don't unescape `_` in labels/URLs and in HTML mode #130

Closed digama0 closed 9 months ago

digama0 commented 9 months ago

fixes #128, fixes #131, supercedes #129. Rather than turning off the diagnostic, the right solution is to not be undoubling _ inside labels/URLs. This means that we now have three different undoubling functions, since the undoubling behavior is different between Text, Label/Url and Math. metamath/metamath-exe@270e86d double checks that metamath.exe in fact does not undouble _ in labels and URLs.

digama0 commented 9 months ago

As for HTML, the solution is similar but more complicated, because underscore undoubling in Text depends on whether it is in HTML mode or not.

tirix commented 9 months ago

For HTML, the solution I propose in #129 seems simpler, since unescape_text should not be called in HTML mode.

digama0 commented 9 months ago

It should, because the other characters are still undoubled in HTML mode. (Observe this by running HTML generation on something like <HTML> [[ ~~ `` __ </HTML> in metamath.exe)

digama0 commented 9 months ago

The plot thickens: I tried the test above, and [ isn't getting undoubled (either in HTML mode or out). In fact I can't get [foo] to link at all. Maybe metamath.exe got broken by the recent change?

tirix commented 9 months ago

In any case tests with[[ and ~~ within HTML should be added in the metamath-exe test suite.

digama0 commented 9 months ago

Turns out that [[ was only getting undoubled if there is a bibliography present. :roll_eyes: