Skip to content

help language: <HTML> #175

New issue
New issue
Open
Open
help language: <HTML>#175
@icecream17

Description

@icecream17
icecream17
opened on Aug 23, 2024

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. $)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions