-
Notifications
You must be signed in to change notification settings - Fork 89
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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 😄. 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.
- Loading branch information
Showing
51 changed files
with
1,048 additions
and
1,046 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.