Sidebar and index overhaul
This commit includes multiple modifications:
Trees
----------
Odoc used to have several representations of trees: one for the page sidebar in
the model, one for the document sidebar, and (in a squashed commit) one for the
unit sidebar.
All trees now have the same type, making the different passes (eg model ->
document for pages and units) much easier, at a small cost (the type is less
tailored to the usecase, eg the payload cannot be different in leafs than in
node, which was the case before in the page hierarchy).
Trees (and forests) have basic iterators defined.
The index for units
------------------------
The index for the units values used to be a hashtable from ID to entry. The
problem was that you cannot rebuild a sidebar from that: you lose the order
between children.
The index for units now is a tree of index entries.
The sidebar for units
-------------------------
The sidebar for units finally shows more than just the root module.
However, it does not show the full hierarchy either, as that would be
overwhelming in the case of big modules.
The sidebar shows:
- Only entries that could have had an expansion: modules, modules types, classes
and class types.
- The current page (highlighted),
- The children of the current page, (highlighted differently),
- The ancestors of the current page,
- The children of the ancestors of the current page,
- Nothing else.
If you allow me, I like to use the github syntax for mathematics :smile:. The
sidebar has the property that it displays the smallest set $S$ that:
- Contains only modules, modules types, classes and class types.
- Contains the current page: $current\_page\in S$,
- Is ancestor-closed: if $e\in S$ then $parent(e)\in S$,
- Is sibling-closed: if $e\in S$ and $parent(e)=parent(f)$, then $f\in S$
The last property is important to avoid displaying only part of the children of
a parent, requiring to display some `...` to show that some entries were
omitted.
Organization in directories and libraries
-----------------------------------------------------
The `search/` folder and its associated `odoc_search` library was separated in
two: the original one and the new `index/` and `odoc_index` which contains
everything that an index should contain: both the info for the sidebar and for
the search index.
82c4d0
-
Jan 01 00:00 +00:00