search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 9 forks source link

add comment markup parser #67

Closed digama0 closed 2 years ago

digama0 commented 2 years ago

This lets us parse metamath's pseudo-markdown syntax in comments:

$( You can do _italics_, sub_scripts, <HTML>(basically <B>verbatim</b>)</HTML> blocks,
   ~ label references and ~ http://web-site.com references, and ` ( math + strings ) ` .

   Also paragraph breaks and [Biblio] references.

   This last bit is not parsed, these markers are handled separately from markup parsing:
   (Contributed by Mario Carneiro, 28-Jan-2022.) $)
foo $a |- ( ph -> ph ) $.
tirix commented 2 years ago

Excellent! I was rather assuming parsing comments would be done outside the library, and had been parsing those in metamath-web using regular expressions, but this works very well too.

digama0 commented 2 years ago

There is a bunch of careful ordering to get right with comment markup (like how some markup works in some nested contexts but not others), so I thought it important to have a dedicated parser to make it easier to get right.

digama0 commented 2 years ago

In order to avoid too many dependent PRs piling up, since the review seems more or less finished, I'm going to merge this now and we can make edits later if necessary.

tirix commented 2 years ago

Sure! Maybe I'll try to make a PR with the API I think would be better (i.e. one without referencing the segments and their buffers directly).