search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
78 stars 25 forks source link

`help language`: `<HTML>` #175

Open icecream17 opened 2 months ago

icecream17 commented 2 months ago

The end of the help language command states that </HTML> is obsolete, and additionally the entire comment is interpreted as html instead of just the values in between the <HTML> and </HTML> tags. https://github.com/metamath/metamath-exe/blob/50179d3e3f980af5f307cf258f86680c8589642d/src/mmhlpa.c#L566-L574

However, this comment states otherwise: https://github.com/metamath/metamath-exe/blob/50179d3e3f980af5f307cf258f86680c8589642d/src/mmwtex.c#L1878

There's also a comment in set.mm, after hypothesis inf3.1 it reads:

  ${
    $d x y w $.
    inf3.1 $e |- E. x ( x =/= (/) /\ x C_ U. x ) $.
    $( Note: the special <HTML> tag is handled in mmwtex.c.  All comment text
       between <HTML> and </HTML> is passed as-is to the web page, except
       that ` (symbols) ` , ~ (label) , and [(reference)] markups are still
       interpreted. $)
digama0 commented 2 months ago

As far as I know, is not obsolete and I've been maintaining tools working under the assumption that it operates as described in the ~inf3 comment.