Skip to content

Commit 988a34a

Browse files
UrgauUrgau
committed
Add per page TOC in the rustc book
1 parent 191df20 commit 988a34a

File tree

3 files changed

+224
-0
lines changed

3 files changed

+224
-0
lines changed

Diff for: ‎src/doc/rustc/book.toml

+2
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ title = "The rustc book"
66
[output.html]
77
git-repository-url = "https://github.com/rust-lang/rust/tree/master/src/doc/rustc"
88
edit-url-template = "https://github.com/rust-lang/rust/edit/master/src/doc/rustc/{path}"
9+
additional-css = ["theme/pagetoc.css"]
10+
additional-js = ["theme/pagetoc.js"]
911

1012
[output.html.search]
1113
use-boolean-and = true

Diff for: ‎src/doc/rustc/theme/pagetoc.css

+104
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
/* Inspidred by https://github.com/JorelAli/mdBook-pagetoc/ */
2+
3+
:root {
4+
--toc-width: 270px;
5+
--center-content-toc-shift: calc(-1 * var(--toc-width) / 2);
6+
}
7+
8+
.nav-chapters {
9+
/* adjust width of buttons that bring to the previous or the next page */
10+
min-width: 50px;
11+
}
12+
13+
.previous {
14+
/*
15+
adjust the space between the left sidebar or the left side of the screen
16+
and the button that leads to the previous page
17+
*/
18+
margin-left: var(--page-padding);
19+
}
20+
21+
@media only screen {
22+
main {
23+
display: -webkit-box;
24+
display: -ms-flexbox;
25+
display: flex;
26+
}
27+
28+
@media (max-width: 1179px) {
29+
.sidebar-hidden #sidetoc {
30+
display: none;
31+
}
32+
}
33+
34+
@media (max-width: 1439px) {
35+
.sidebar-visible #sidetoc {
36+
display: none;
37+
}
38+
}
39+
40+
@media (1180px <= width <= 1439px) {
41+
.sidebar-hidden main {
42+
position: relative;
43+
left: var(--center-content-toc-shift);
44+
}
45+
}
46+
47+
@media (1440px <= width <= 1700px) {
48+
.sidebar-visible main {
49+
position: relative;
50+
left: var(--center-content-toc-shift);
51+
}
52+
}
53+
54+
.content-wrap {
55+
width: 100%;
56+
}
57+
58+
#sidetoc {
59+
margin-top: 20px;
60+
margin-left: 20px;
61+
margin-right: auto;
62+
}
63+
#pagetoc {
64+
position: fixed;
65+
/* adjust TOC width */
66+
width: var(--toc-width);
67+
height: calc(100vh - var(--menu-bar-height) - 0.67em * 4);
68+
overflow: auto;
69+
}
70+
#pagetoc a {
71+
border-left: 1px solid var(--sidebar-bg);
72+
color: var(--sidebar-fg) !important;
73+
display: block;
74+
padding-bottom: 5px;
75+
padding-top: 5px;
76+
padding-left: 10px;
77+
text-align: left;
78+
text-decoration: none;
79+
}
80+
#pagetoc a:hover,
81+
#pagetoc a.active {
82+
background: var(--sidebar-bg);
83+
color: var(--sidebar-active) !important;
84+
}
85+
#pagetoc .active {
86+
background: var(--sidebar-bg);
87+
color: var(--sidebar-active);
88+
}
89+
#pagetoc .pagetoc-H2 {
90+
padding-left: 20px;
91+
}
92+
#pagetoc .pagetoc-H3 {
93+
padding-left: 40px;
94+
}
95+
#pagetoc .pagetoc-H4 {
96+
padding-left: 60px;
97+
}
98+
}
99+
100+
@media print {
101+
#sidetoc {
102+
display: none;
103+
}
104+
}

Diff for: ‎src/doc/rustc/theme/pagetoc.js

+118
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
// Inspired by https://github.com/JorelAli/mdBook-pagetoc/
2+
3+
let activeHref = location.href;
4+
function updatePageToc(elem = undefined) {
5+
let selectedPageTocElem = elem;
6+
const pagetoc = document.getElementById("pagetoc");
7+
8+
function getRect(element) {
9+
return element.getBoundingClientRect();
10+
}
11+
12+
function overflowTop(container, element) {
13+
return getRect(container).top - getRect(element).top;
14+
}
15+
16+
function overflowBottom(container, element) {
17+
return getRect(container).bottom - getRect(element).bottom;
18+
}
19+
20+
// We've not selected a heading to highlight, and the URL needs updating
21+
// so we need to find a heading based on the URL
22+
if (selectedPageTocElem === undefined && location.href !== activeHref) {
23+
activeHref = location.href;
24+
for (const pageTocElement of pagetoc.children) {
25+
if (pageTocElement.href === activeHref) {
26+
selectedPageTocElem = pageTocElement;
27+
}
28+
}
29+
}
30+
31+
// We still don't have a selected heading, let's try and find the most
32+
// suitable heading based on the scroll position
33+
if (selectedPageTocElem === undefined) {
34+
const margin = window.innerHeight / 3;
35+
36+
const headers = document.getElementsByClassName("header");
37+
for (let i = 0; i < headers.length; i++) {
38+
const header = headers[i];
39+
if (selectedPageTocElem === undefined && getRect(header).top >= 0) {
40+
if (getRect(header).top < margin) {
41+
selectedPageTocElem = header;
42+
} else {
43+
selectedPageTocElem = headers[Math.max(0, i - 1)];
44+
}
45+
}
46+
// a very long last section's heading is over the screen
47+
if (selectedPageTocElem === undefined && i === headers.length - 1) {
48+
selectedPageTocElem = header;
49+
}
50+
}
51+
}
52+
53+
// Remove the active flag from all pagetoc elements
54+
for (const pageTocElement of pagetoc.children) {
55+
pageTocElement.classList.remove("active");
56+
}
57+
58+
// If we have a selected heading, set it to active and scroll to it
59+
if (selectedPageTocElem !== undefined) {
60+
for (const pageTocElement of pagetoc.children) {
61+
if (selectedPageTocElem.href.localeCompare(pageTocElement.href) === 0) {
62+
pageTocElement.classList.add("active");
63+
if (overflowTop(pagetoc, pageTocElement) > 0) {
64+
pagetoc.scrollTop = pageTocElement.offsetTop;
65+
}
66+
if (overflowBottom(pagetoc, pageTocElement) < 0) {
67+
pagetoc.scrollTop -= overflowBottom(pagetoc, pageTocElement);
68+
}
69+
}
70+
}
71+
}
72+
}
73+
74+
if (document.getElementById("sidetoc") === null) {
75+
// Element doesn't exist yet, let's create it
76+
const main = document.querySelector('main');
77+
const wrapper = document.createElement('div');
78+
wrapper.className = "content-wrap";
79+
80+
// Move all children into the wrapper
81+
while (main.firstChild) {
82+
wrapper.appendChild(main.firstChild);
83+
}
84+
85+
// Append the wrapper back to main
86+
main.appendChild(wrapper);
87+
88+
// Create the empty sidetoc and pagetoc elements
89+
const sidetoc = document.createElement("div");
90+
const pagetoc = document.createElement("div");
91+
sidetoc.id = "sidetoc";
92+
pagetoc.id = "pagetoc";
93+
94+
// And append them to the current DOM
95+
sidetoc.appendChild(pagetoc);
96+
main.appendChild(sidetoc);
97+
}
98+
99+
if (document.getElementsByClassName("header").length <= 1) {
100+
// There's one or less headings, we don't need a page table of contents
101+
document.getElementById("sidetoc").remove();
102+
} else {
103+
// Populate sidebar on load
104+
window.addEventListener("load", () => {
105+
for (const header of document.getElementsByClassName("header")) {
106+
const link = document.createElement("a");
107+
link.innerHTML = header.innerHTML;
108+
link.href = header.hash;
109+
link.classList.add("pagetoc-" + header.parentElement.tagName);
110+
document.getElementById("pagetoc").appendChild(link);
111+
link.onclick = () => updatePageToc(link);
112+
}
113+
updatePageToc();
114+
});
115+
116+
// Update page table of contents selected heading on scroll
117+
window.addEventListener("scroll", () => updatePageToc());
118+
}

0 commit comments

Comments
 (0)