request: in docs of a repository, display that repository differently from its dependencies

[hrmacbeth]

In the doc-gen for mathlib3, the left sidebar looks like this:

core
▸ data
▸ init
▸ system

mathlib
▸ algebra
▸ algebraic_geometry
▸ algebraic_topology
▸ analysis
▸ category theory
...

That is, the repo we have actually run doc-gen on (mathlib) and its dependencies (core) are displayed as headings and all of their top-level folders are displayed afterwards in a list. I like this feature because I spend a lot of time browsing mathlib and this saves me a click. Mathlib hierarchies also get pretty deep, so having all the mathlib top-level folders left-justified also saves a few indentation characters which comes in handy deeper down.

In the doc-gen for mathlib4, the left sidebar looks like this:

▸ Init
▸ Lean
▸ Mathlib
▸ Std

I can see why @hargoniX made this choice, because now the dependencies (Init, Lean and Std) all have many top-level folders, and displaying all of these would push the top-level folders from the repo of interest (Mathlib) far off-screen!

It's still annoying to have the extra click, though (and this is exacerbated by the issue in #99 causing the valid clickable region to be a single unicode symbol ▸).

Here is a more complicated proposal which I think would be the best of both worlds: first display the dependencies, with just their names, then display all the top-level folders of the repository of interest. So

▸ Init
▸ Lean
▸ Std

---

Mathlib
▸ Algebra
▸ CategoryTheory
▸ Combinatorics
▸ Control
...