If you want to learn how to do the web site generation, you might find https://github.com/digama0/mm-web-rs/blob/master/src/render.rs, along with https://github.com/metamath/metamath-knife/blob/main/metamath-rs/src/comment_parser.rs, valuable for understanding how comments are parsed and then rendered as HTML. In this case, I believe that the comment is in a <HTML> block, and this disables the parsing of line breaks (tags are treated as is so you need a <p> tag after each paragraph). I will double check what mm-web-rs does here, but it might be that metamath-exe doesn't actually respect <HTML> boundaries and just treats the whole comment as if it was in such a block. It seems like a bug.
Parsing ~, [ and ` is a bit of a nightmare. I recommend just copying what comment_parser.rs does. On Wed, Sep 3, 2025 at 6:28 PM Marlo Bruder <[email protected]> wrote: > Hello everyone, > > I recently got around to implementing description parsing (for my proof > assistant), as it is described in > https://us.metamath.org/downloads/metamath.pdf#subsection.4.4.1 and I had > a few question that I was hoping some of you might be able to answer. > > > 1. What is the condition for a new paragraph to begin? I thought that > the condition might be at least one line of whitespace, but then I had a > look at theorem a1ii ( https://us.metamath.org/mpeuni/a1ii.html ) and > noticed that what should be 3 paragraph (if you take a look at the > set.mm source file) are rendered as one. Funnily enough the 2 > paragraphs below the html adhere to the rule mentioned above, so I'm not > really sure what exactly the condition is. > 2. I noticed that theorem ex-natded5.2 ( > https://us.metamath.org/mpeuni/ex-natded5.2.html ) has an "a" html-tag > in it's description that is not surrounded by an "html" html-tag. Despite > of that on the webpage it is rendered as a link. How is this possible? The > metamath-book makes no mention of this. > 3. Some of the text in the section linked above seems a bit unclear. > For example: It says that "`" starts and ends math mode, but at the same > time "~" is supposed to convert everything up to the next whitespace to a > label. What if these happen at the same time though? What if you have > something like "~test` "? Is the "`" supposed to start math mode or beome > part of the label? The same thing applies to cases like "~test1~test2" (1 > or 2 labels?) or "_test~test_" (italic or italic + label?). > > Thanks for any answers in advance!!! > > Best regards, > Marlo Bruder > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/ce84b83f-d30d-4a09-b53b-2b1cdc171643n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/ce84b83f-d30d-4a09-b53b-2b1cdc171643n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSvOzxP3farLh8R_ZMNgxiO2wTqHSagNeMPiAMQrLJGZoA%40mail.gmail.com.
