Skip to content

Commit 8fcff8c

Browse files
UrgauUrgau
committed
Add per page TOC in the rustc book
1 parent 414482f commit 8fcff8c

3 files changed

Lines changed: 224 additions & 0 deletions

File tree

‎src/doc/rustc/book.toml‎

Lines changed: 2 additions & 0 deletions
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‎

Lines changed: 104 additions & 0 deletions
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+
: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+
@mediaonly 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-hiddenmain {
42+
position: relative;
43+
left:var(--center-content-toc-shift);
44+
}
45+
}
46+
47+
@media (1440px <= width <= 1700px) {
48+
.sidebar-visiblemain {
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+
#pagetoca {
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+
#pagetoca:hover,
81+
#pagetoca.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+
}

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

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
// Inspired by https://github.com/JorelAli/mdBook-pagetoc/tree/98ee241 (under WTFPL)
2+
3+
letactiveHref=location.href;
4+
functionupdatePageToc(elem=undefined){
5+
letselectedPageTocElem=elem;
6+
constpagetoc=document.getElementById("pagetoc");
7+
8+
functiongetRect(element){
9+
returnelement.getBoundingClientRect();
10+
}
11+
12+
functionoverflowTop(container,element){
13+
returngetRect(container).top-getRect(element).top;
14+
}
15+
16+
functionoverflowBottom(container,element){
17+
returngetRect(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(constpageTocElementofpagetoc.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+
constmargin=window.innerHeight/3;
35+
36+
constheaders=document.getElementsByClassName("header");
37+
for(leti=0;i<headers.length;i++){
38+
constheader=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(constpageTocElementofpagetoc.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(constpageTocElementofpagetoc.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+
constmain=document.querySelector('main');
77+
constwrapper=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+
constsidetoc=document.createElement("div");
90+
constpagetoc=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(constheaderofdocument.getElementsByClassName("header")){
106+
constlink=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)