search

metamath / metamath-knife

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

Outline #8

Closed tirix closed 3 years ago

tirix commented 3 years ago

This adds support for getting the outline (chapters, sections, sub-sections) of a database. When the database option outline is set, the positions of the chapter headings is computed and stored during parsing. The command line option --outline activates this options and outputs the outline in text format.

david-a-wheeler commented 3 years ago

Awesome! I'm trying to spend some time "off the computer" for the holidays, but I thank you profusely. I'll look at this more in a little bit.

tirix commented 3 years ago

@david-a-wheeler @digama0 would you agree to merge this PR first? Any remark?

digama0 commented 3 years ago

The style is wonky in this one too, but I'll merge it since we're planning to rustfmt in another PR.

david-a-wheeler commented 3 years ago

Yes, it's good to merge & then fix style. Ideally the style is clean at the beginning, but at this juncture this is the efficient way to do it.

Please do propose a rustfmt in a different PR once things have settled.