Skip to content

Commit

Permalink
toc-top is now correct when a sidebar is absent
Browse files Browse the repository at this point in the history
  • Loading branch information
EmileTrotignon committed Nov 8, 2023
1 parent 86c990c commit dd9a39e
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 13 deletions.
9 changes: 7 additions & 2 deletions src/html_support_files/odoc.css
Original file line number Diff line number Diff line change
Expand Up @@ -784,10 +784,15 @@ td.def-doc *:first-child {
line-height: 1.2;
}

.odoc-search + * + .odoc-toc {
--toc-top: calc(var(--search-bar-height) + var(--search-padding-top) + 20px);
max-height: calc(100vh - 2 * var(--toc-top));
top: var(--toc-top)
}

.odoc-toc {
/* TODO : make this smaller if there is no search bar */
--toc-top: calc(var(--search-bar-height) + var(--search-padding-top) + 20px);
--toc-top: 20px;
width: 28ex;
background: var(--toc-background);
overflow: auto;
Expand All @@ -798,10 +803,10 @@ td.def-doc *:first-child {
grid-row-end: 5;
grid-column: 1;
height: fit-content;
max-height: calc(100vh - 2 * var(--toc-top));
border: solid 1px var(--border);
border-radius: 5px;
position:sticky;
max-height: calc(100vh - 2 * var(--toc-top));
top: var(--toc-top)
}

Expand Down
Loading

0 comments on commit dd9a39e

Please sign in to comment.