leanprover / verso

Lean documentation authoring tool
Apache License 2.0
125 stars 14 forks source link

Manual genre: include "points of interest" in left-hand ToC #187

Open david-christiansen opened 1 month ago

david-christiansen commented 1 month ago

As of #186, the manual genre has a much nicer Scribble-inspired table of contents in the left bar.

But it's still missing one important Scribble feature: navigating within the current page. In Scribble, "points of interest" like documented symbols and subsections are listed in the left bar as well. Verso should do this too.

Here's a screenshot. Look where it says "on this page:" image