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

Underscores in comment's Html #129

Closed tirix closed 9 months ago

tirix commented 9 months ago

Originally opened because of #128 to avoid issuing a diagnostic in case a non-doubled underscore is found in an URL.

Changed into fixing the handling of underscores in HTML.

Fixes #131

digama0 commented 9 months ago

not issuing the diagnostic is incorrect, if we are in fact undoubling underscores. The point of the diagnostic is that if __ will be turned into _ then _ alone is probably an error, even though it will be preserved.

tirix commented 9 months ago

not issuing the diagnostic is incorrect, if we are in fact undoubling underscores.

Indeed in CommentItem comment section, unescape_text is supposed to be run for Urls. In that case, the issue #128 is not an issue and does not need to be fixed. In set.mm however, no underscore is doubled in Urls. This boils down to what we want the standard to be.

tirix commented 9 months ago

I'm making use of this PR to fix the behaviour of underscores in HTML (sorry for the change, I hope it's not a too bad practice)

The comments clearly states:

In HTML mode subscripts and italics are disabled, and HTML markup is interpreted

So there is no point to escaping underscores in HTML mode.

tirix commented 9 months ago

Superseded by #130 .