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.
