ordering of sidebar links in docs

Stream: general

[Matt Diamond]

I've noticed that the links to individual theorems/definitions on the right side of the Lean 4 docs are listed in the order they're defined in rather than alphabetical order (which is how they're ordered in the Lean 3 docs). I feel like the alphabetical ordering was more useful and I'm wondering if anyone else feels this way. Has this been previously discussed? Could this be changed?

[Henrik Böving]

Has this been previously discussed?

no, but you should discuss it if you dont like it.

Could this be changed?

yes

[Matt Diamond]

you should discuss it if you dont like it.

Gotcha. My perspective is that an alphabetical sidebar is useful for quick lookups. I'm thinking of a scenario where you're browsing a page and you'd like to see if a specific lemma/def is on that page, or maybe you know it is and you want to jump to it quickly. Or a scenario where you want to see which lemmas/defs on that page have a specific prefix. An alphabetical listing is helpful in these scenarios, whereas a non-alphabetical listing is useless.

Obviously there are other ways to handle these scenarios, like using the search bar or Command-F, but IMHO having an alphabetical listing provides a useful overview of the contents of a file.

[Kyle Miller]

Here's a UI proposal:

• Have radio buttons in the right sidebar at the top of the list of declarations, (*) Outline ( ) A-Z
• In Outline mode, it's the same as now, but it also includes the section headings that appear in the documentation (with the appropriate CSS style so that they get truncated with an ellipsis and stay each on one line perhaps, and a tooltip with the full heading?)
• In A-Z mode, it shows the declarations in alphabetical order. (No headings are included, that wouldn't make sense)
• We develop some unobtrusive icons to list next to each declaration to show whether each declaration is a definition, a theorem, an inductive type, or something else. (A simple design: a ~2px vertical bar with the same color of the corresponding declaration type used in the main body of the documentation.)

[Matt Diamond]

I like it! I would add that the mode should stay consistent when navigating to different pages (as opposed to always starting in Outline mode).

[Yaël Dillies]

Why only allow reordering the sidebar? Could we also reorder the main body too?

[Eric Wieser]

What would that do with doc comments?

[Yaël Dillies]

Discard them in all views but the default one.