leanprover / verso

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

Manual genre: navigation buttons should be a preorder traversal #231

Closed david-christiansen closed 1 week ago

david-christiansen commented 1 week ago

Today, the navigation buttons "prev" and "next" navigate the structure of the tree, going to sibling nodes. Thus, "next" means "next chapter" when looking at a chapter, or "next subsubsection" when looking at a subsubsection.

They should instead navigate via a preorder traversal of the tree, so "next" at the root opens chapter 1, "next" from there goes to chapter 1 section 1. Because there's no 1.1.1, "next" then goes to chapter 1 section 2, and then to chapter 2 if that's the last node in chapter 1. In other words, this is like turning the page of a physical book.