Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

help language: <HTML> #175

Open
icecream17 opened this issue Aug 23, 2024 · 1 comment
Open

help language: <HTML> #175

icecream17 opened this issue Aug 23, 2024 · 1 comment

Comments

@icecream17
Copy link

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.

metamath-exe/src/mmhlpa.c

Lines 566 to 574 in 50179d3

H(" <HTML> - A comment containing \"<HTML>\" (case-sensitive) is");
H(" bypassed by the algorithm of SHOW PROOF ... / REWRAP. Also,");
H(" \"<\" is not converted to \"&lt;\" by the algorithm. The");
H(" \"<HTML>\" is discarded in the generated web page. Any");
H(" \"</HTML>\" (deprecated) is discarded and ignored. Note that");
H(" the entire comment (not just sections delineated by");
H(" \"<HTML>...</HTML>\") is treated as HTML code if any");
H(" \"<HTML>\" is present anywhere in the comment.");
H(" See also HELP WRITE SOURCE for more information.");

However, this comment states otherwise:

metamath-exe/src/mmwtex.c

Line 1878 in 50179d3

// Don't modify anything inside of <HTML>...</HTML> tags

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
Copy link
Member

digama0 commented Aug 24, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@digama0 @icecream17