Skip to content

Commit 9b510aa

Browse files
rust-timerrust-timer
authored
Unrolled build for rust-lang#140113
Rollup merge of rust-lang#140113 - Urgau:rustc-book-page-toc, r=ehuss Add per page TOC in the `rustc` book This PR adds per page Table of Content (TOC) in the `rustc` book (to be extended in the future to our other books). The goal is to easy the navigation inside the page by providing quick overview of the page content and our position inside that page. That functionality is unfortunately not available natively in `mdbook`, which prompted community members to create [mdBook-pagetoc](https://github.com/JorelAli/mdBook-pagetoc/) (which this PR is heavily inspired by). It's "only" a JS file (to handle the TOC) and a CSS file (to handle the margin, colors, screen size, ...), there is no "post-processor" needed (in mdbook sense). ![image](https://github.com/user-attachments/assets/9e790bea-059d-414e-b4a5-ac8170f57e27) Live preview at: http://urgau.rf.gd/book r? ```@jieyouxu```
2 parents 7205fc5 + 4cbcb44 commit 9b510aa

File tree

3 files changed

+190
-0
lines changed

3 files changed

+190
-0
lines changed

‎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

‎src/doc/rustc/theme/pagetoc.css

+84
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
/* Inspired by https://github.com/JorelAli/mdBook-pagetoc/tree/98ee241 (under WTFPL) */
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+
@media only screen {
14+
@media (max-width: 1179px) {
15+
.sidebar-hidden #sidetoc {
16+
display: none;
17+
}
18+
}
19+
20+
@media (max-width: 1439px) {
21+
.sidebar-visible #sidetoc {
22+
display: none;
23+
}
24+
}
25+
26+
@media (1180px <= width <= 1439px) {
27+
.sidebar-hidden main {
28+
position: relative;
29+
left: var(--center-content-toc-shift);
30+
}
31+
}
32+
33+
@media (1440px <= width <= 1700px) {
34+
.sidebar-visible main {
35+
position: relative;
36+
left: var(--center-content-toc-shift);
37+
}
38+
}
39+
40+
#sidetoc {
41+
margin-left: calc(100% + 20px);
42+
}
43+
#pagetoc {
44+
position: fixed;
45+
/* adjust TOC width */
46+
width: var(--toc-width);
47+
height: calc(100vh - var(--menu-bar-height) - 0.67em * 4);
48+
overflow: auto;
49+
}
50+
#pagetoc a {
51+
border-left: 1px solid var(--sidebar-bg);
52+
color: var(--sidebar-fg) !important;
53+
display: block;
54+
padding-bottom: 5px;
55+
padding-top: 5px;
56+
padding-left: 10px;
57+
text-align: left;
58+
text-decoration: none;
59+
}
60+
#pagetoc a:hover,
61+
#pagetoc a.active {
62+
background: var(--sidebar-bg);
63+
color: var(--sidebar-active) !important;
64+
}
65+
#pagetoc .active {
66+
background: var(--sidebar-bg);
67+
color: var(--sidebar-active);
68+
}
69+
#pagetoc .pagetoc-H2 {
70+
padding-left: 20px;
71+
}
72+
#pagetoc .pagetoc-H3 {
73+
padding-left: 40px;
74+
}
75+
#pagetoc .pagetoc-H4 {
76+
padding-left: 60px;
77+
}
78+
}
79+
80+
@media print {
81+
#sidetoc {
82+
display: none;
83+
}
84+
}

‎src/doc/rustc/theme/pagetoc.js

+104
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
// Inspired by https://github.com/JorelAli/mdBook-pagetoc/tree/98ee241 (under WTFPL)
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+
document.getElementsByClassName("header").length > 0) {
76+
// The sidetoc element doesn't exist yet, let's create it
77+
78+
// Create the empty sidetoc and pagetoc elements
79+
const sidetoc = document.createElement("div");
80+
const pagetoc = document.createElement("div");
81+
sidetoc.id = "sidetoc";
82+
pagetoc.id = "pagetoc";
83+
sidetoc.appendChild(pagetoc);
84+
85+
// And append them to the current DOM
86+
const main = document.querySelector('main');
87+
main.insertBefore(sidetoc, main.firstChild);
88+
89+
// Populate sidebar on load
90+
window.addEventListener("load", () => {
91+
for (const header of document.getElementsByClassName("header")) {
92+
const link = document.createElement("a");
93+
link.innerHTML = header.innerHTML;
94+
link.href = header.hash;
95+
link.classList.add("pagetoc-" + header.parentElement.tagName);
96+
document.getElementById("pagetoc").appendChild(link);
97+
link.onclick = () => updatePageToc(link);
98+
}
99+
updatePageToc();
100+
});
101+
102+
// Update page table of contents selected heading on scroll
103+
window.addEventListener("scroll", () => updatePageToc());
104+
}

0 commit comments

Comments
 (0)