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 ...