Questions about description parsing

39 views
Skip to first unread message

Marlo Bruder

unread,
Sep 3, 2025, 12:28:14 PMSep 3
to Metamath
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

Mario Carneiro

unread,
Sep 3, 2025, 4:24:39 PMSep 3
to meta...@googlegroups.com
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.

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/ce84b83f-d30d-4a09-b53b-2b1cdc171643n%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages