search

metamath / metamath-knife

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

Doubling underscores in HTML mode #131

Closed tirix closed 1 year ago

tirix commented 1 year ago

metamath-knife produces an error on the following:

$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
  Goldbach's conjectures
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-

  <HTML>
  to distinguish it from a weaker conjecture, known ... as the
  _Goldbach's weak conjecture_, the _odd Goldbach conjecture_, or the _ternary
  Goldbach conjecture_.  This weak conjecture asserts that all odd numbers

The error is:

warning: Invalid escape character
      --> ../set.mm/set.mm:729762:3
       |
729762 |   _Goldbach's weak conjecture_, the _odd Goldbach conjecture_, or the _ternary
       |   - This escape character should be doubled
       |
       = note: This character has special meaning in this position, but it was not interpretable here.
       = note: Use ~~ or [[ or `` if you mean to include the character literally

However, underscores don't need to be doubled in HTML mode, since:

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

digama0 commented 1 year ago

I hope that's a contrived example, because that is an incorrect use of _, since it is clearly trying to do italics but this doesn't work in HTML mode.

tirix commented 1 year ago

That's an actual part of set.mm. In the page generated by metamath-exe, underscores are untouched. Obviously this tries to do italics in HTML mode, which should be achieved with the <em> tag instead.