Skip to content

Commit 3ed25f9

Browse files
Update gh-pages
Store path: /nix/store/kj8qafklwsnfjwphniy8nx2yzgfx4xhc-docs
1 parent 9e29e5d commit 3ed25f9

15 files changed

+296
-227
lines changed

404.html

+18-39
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
<!DOCTYPE HTML>
2-
<html lang="en" class="light" dir="ltr">
2+
<html lang="en" class="light sidebar-visible" dir="ltr">
33
<head>
44
<!-- Book generated using mdBook -->
55
<meta charset="UTF-8">
@@ -8,7 +8,7 @@
88

99

1010
<!-- Custom HTML head -->
11-
11+
1212
<meta name="description" content="">
1313
<meta name="viewport" content="width=device-width, initial-scale=1">
1414
<meta name="theme-color" content="#ffffff">
@@ -31,15 +31,17 @@
3131

3232
<!-- Custom theme stylesheets -->
3333

34-
</head>
35-
<body class="sidebar-visible no-js">
36-
<div id="body-container">
34+
3735
<!-- Provide site root to javascript -->
3836
<script>
3937
var path_to_root = "";
4038
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
4139
</script>
42-
40+
<!-- Start loading toc.js asap -->
41+
<script src="toc.js"></script>
42+
</head>
43+
<body>
44+
<div id="body-container">
4345
<!-- Work around some values being stored in localStorage wrapped in quotes -->
4446
<script>
4547
try {
@@ -61,19 +63,16 @@
6163
var theme;
6264
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
6365
if (theme === null || theme === undefined) { theme = default_theme; }
64-
var html = document.querySelector('html');
66+
const html = document.documentElement;
6567
html.classList.remove('light')
6668
html.classList.add(theme);
67-
var body = document.querySelector('body');
68-
body.classList.remove('no-js')
69-
body.classList.add('js');
69+
html.classList.add("js");
7070
</script>
7171

7272
<input type="checkbox" id="sidebar-toggle-anchor" class="hidden">
7373

7474
<!-- Hide / unhide sidebar before it is displayed -->
7575
<script>
76-
var body = document.querySelector('body');
7776
var sidebar = null;
7877
var sidebar_toggle = document.getElementById("sidebar-toggle-anchor");
7978
if (document.body.clientWidth >= 1080) {
@@ -83,45 +82,25 @@
8382
sidebar = 'hidden';
8483
}
8584
sidebar_toggle.checked = sidebar === 'visible';
86-
body.classList.remove('sidebar-visible');
87-
body.classList.add("sidebar-" + sidebar);
85+
html.classList.remove('sidebar-visible');
86+
html.classList.add("sidebar-" + sidebar);
8887
</script>
8988

9089
<nav id="sidebar" class="sidebar" aria-label="Table of contents">
91-
<div class="sidebar-scrollbox">
92-
<ol class="chapter"><li class="chapter-item expanded "><a href="introduction.html"><strong aria-hidden="true">1.</strong> Introduction</a></li><li class="chapter-item expanded "><a href="documentation.html"><strong aria-hidden="true">2.</strong> Documentation</a></li></ol>
93-
</div>
90+
<!-- populated by js -->
91+
<mdbook-sidebar-scrollbox class="sidebar-scrollbox"></mdbook-sidebar-scrollbox>
92+
<noscript>
93+
<iframe class="sidebar-iframe-outer" src="toc.html"></iframe>
94+
</noscript>
9495
<div id="sidebar-resize-handle" class="sidebar-resize-handle">
9596
<div class="sidebar-resize-indicator"></div>
9697
</div>
9798
</nav>
9899

99-
<!-- Track and set sidebar scroll position -->
100-
<script>
101-
var sidebarScrollbox = document.querySelector('#sidebar .sidebar-scrollbox');
102-
sidebarScrollbox.addEventListener('click', function(e) {
103-
if (e.target.tagName === 'A') {
104-
sessionStorage.setItem('sidebar-scroll', sidebarScrollbox.scrollTop);
105-
}
106-
}, { passive: true });
107-
var sidebarScrollTop = sessionStorage.getItem('sidebar-scroll');
108-
sessionStorage.removeItem('sidebar-scroll');
109-
if (sidebarScrollTop) {
110-
// preserve sidebar scroll position when navigating via links within sidebar
111-
sidebarScrollbox.scrollTop = sidebarScrollTop;
112-
} else {
113-
// scroll sidebar to current active section when navigating via "next/previous chapter" buttons
114-
var activeSection = document.querySelector('#sidebar .active');
115-
if (activeSection) {
116-
activeSection.scrollIntoView({ block: 'center' });
117-
}
118-
}
119-
</script>
120-
121100
<div id="page-wrapper" class="page-wrapper">
122101

123102
<div class="page">
124-
<div id="menu-bar-hover-placeholder"></div>
103+
<div id="menu-bar-hover-placeholder"></div>
125104
<div id="menu-bar" class="menu-bar sticky">
126105
<div class="left-buttons">
127106
<label id="sidebar-toggle" class="icon-button" for="sidebar-toggle-anchor" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">

book.js

+9-16
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,7 @@ function playground_text(playground, hidden = true) {
225225
}
226226

227227
var clipButton = document.createElement('button');
228-
clipButton.className = 'fa fa-copy clip-button';
228+
clipButton.className = 'clip-button';
229229
clipButton.title = 'Copy to clipboard';
230230
clipButton.setAttribute('aria-label', clipButton.title);
231231
clipButton.innerHTML = '<i class=\"tooltiptext\"></i>';
@@ -258,7 +258,7 @@ function playground_text(playground, hidden = true) {
258258

259259
if (window.playground_copyable) {
260260
var copyCodeClipboardButton = document.createElement('button');
261-
copyCodeClipboardButton.className = 'fa fa-copy clip-button';
261+
copyCodeClipboardButton.className = 'clip-button';
262262
copyCodeClipboardButton.innerHTML = '<i class="tooltiptext"></i>';
263263
copyCodeClipboardButton.title = 'Copy to clipboard';
264264
copyCodeClipboardButton.setAttribute('aria-label', copyCodeClipboardButton.title);
@@ -289,6 +289,10 @@ function playground_text(playground, hidden = true) {
289289
var themeToggleButton = document.getElementById('theme-toggle');
290290
var themePopup = document.getElementById('theme-list');
291291
var themeColorMetaTag = document.querySelector('meta[name="theme-color"]');
292+
var themeIds = [];
293+
themePopup.querySelectorAll('button.theme').forEach(function (el) {
294+
themeIds.push(el.id);
295+
});
292296
var stylesheets = {
293297
ayuHighlight: document.querySelector("[href$='ayu-highlight.css']"),
294298
tomorrowNight: document.querySelector("[href$='tomorrow-night.css']"),
@@ -317,7 +321,7 @@ function playground_text(playground, hidden = true) {
317321
function get_theme() {
318322
var theme;
319323
try { theme = localStorage.getItem('mdbook-theme'); } catch (e) { }
320-
if (theme === null || theme === undefined) {
324+
if (theme === null || theme === undefined || !themeIds.includes(theme)) {
321325
return default_theme;
322326
} else {
323327
return theme;
@@ -459,17 +463,6 @@ function playground_text(playground, hidden = true) {
459463
try { localStorage.setItem('mdbook-sidebar', 'visible'); } catch (e) { }
460464
}
461465

462-
463-
var sidebarAnchorToggles = document.querySelectorAll('#sidebar a.toggle');
464-
465-
function toggleSection(ev) {
466-
ev.currentTarget.parentElement.classList.toggle('expanded');
467-
}
468-
469-
Array.from(sidebarAnchorToggles).forEach(function (el) {
470-
el.addEventListener('click', toggleSection);
471-
});
472-
473466
function hideSidebar() {
474467
body.classList.remove('sidebar-visible')
475468
body.classList.add('sidebar-hidden');
@@ -597,12 +590,12 @@ function playground_text(playground, hidden = true) {
597590

598591
function hideTooltip(elem) {
599592
elem.firstChild.innerText = "";
600-
elem.className = 'fa fa-copy clip-button';
593+
elem.className = 'clip-button';
601594
}
602595

603596
function showTooltip(elem, msg) {
604597
elem.firstChild.innerText = msg;
605-
elem.className = 'fa fa-copy tooltipped';
598+
elem.className = 'clip-button tooltipped';
606599
}
607600

608601
var clipboardSnippets = new ClipboardJS('.clip-button', {

css/chrome.css

+45-9
Original file line numberDiff line numberDiff line change
@@ -40,9 +40,9 @@ a > .hljs {
4040
border-block-end-style: solid;
4141
}
4242
#menu-bar.sticky,
43-
.js #menu-bar-hover-placeholder:hover + #menu-bar,
44-
.js #menu-bar:hover,
45-
.js.sidebar-visible #menu-bar {
43+
#menu-bar-hover-placeholder:hover + #menu-bar,
44+
#menu-bar:hover,
45+
html.sidebar-visible #menu-bar {
4646
position: -webkit-sticky;
4747
position: sticky;
4848
top: 0 !important;
@@ -91,7 +91,7 @@ a > .hljs {
9191
display: flex;
9292
margin: 0 5px;
9393
}
94-
.no-js .left-buttons button {
94+
html:not(.js) .left-buttons button {
9595
display: none;
9696
}
9797

@@ -107,7 +107,7 @@ a > .hljs {
107107
overflow: hidden;
108108
text-overflow: ellipsis;
109109
}
110-
.js .menu-title {
110+
.menu-title {
111111
cursor: pointer;
112112
}
113113

@@ -250,8 +250,8 @@ pre > .buttons i {
250250
pre > .buttons button {
251251
cursor: inherit;
252252
margin: 0px 5px;
253-
padding: 3px 5px;
254-
font-size: 14px;
253+
padding: 4px 4px 3px 5px;
254+
font-size: 23px;
255255

256256
border-style: solid;
257257
border-width: 1px;
@@ -262,6 +262,27 @@ pre > .buttons button {
262262
transition-property: color,border-color,background-color;
263263
color: var(--icons);
264264
}
265+
266+
pre > .buttons button.clip-button {
267+
padding: 2px 4px 0px 6px;
268+
}
269+
pre > .buttons button.clip-button::before {
270+
/* clipboard image from octicons (https://github.com/primer/octicons/tree/v2.0.0) MIT license
271+
*/
272+
content: url('data:image/svg+xml,<svg width="21" height="20" viewBox="0 0 24 25" \
273+
xmlns="http://www.w3.org/2000/svg" aria-label="Copy to clipboard">\
274+
<path d="M18 20h2v3c0 1-1 2-2 2H2c-.998 0-2-1-2-2V5c0-.911.755-1.667 1.667-1.667h5A3.323 3.323 0 \
275+
0110 0a3.323 3.323 0 013.333 3.333h5C19.245 3.333 20 4.09 20 5v8.333h-2V9H2v14h16v-3zM3 \
276+
7h14c0-.911-.793-1.667-1.75-1.667H13.5c-.957 0-1.75-.755-1.75-1.666C11.75 2.755 10.957 2 10 \
277+
2s-1.75.755-1.75 1.667c0 .911-.793 1.666-1.75 1.666H4.75C3.793 5.333 3 6.09 3 7z"/>\
278+
<path d="M4 19h6v2H4zM12 11H4v2h8zM4 17h4v-2H4zM15 15v-3l-4.5 4.5L15 21v-3l8.027-.032L23 15z"/>\
279+
</svg>');
280+
filter: var(--copy-button-filter);
281+
}
282+
pre > .buttons button.clip-button:hover::before {
283+
filter: var(--copy-button-filter-hover);
284+
}
285+
265286
@media (pointer: coarse) {
266287
pre > .buttons button {
267288
/* On mobile, make it easier to tap buttons. */
@@ -399,15 +420,30 @@ ul#searchresults span.teaser em {
399420
background-color: var(--sidebar-bg);
400421
color: var(--sidebar-fg);
401422
}
423+
.sidebar-iframe-inner {
424+
background-color: var(--sidebar-bg);
425+
color: var(--sidebar-fg);
426+
padding: 10px 10px;
427+
margin: 0;
428+
font-size: 1.4rem;
429+
}
430+
.sidebar-iframe-outer {
431+
border: none;
432+
height: 100%;
433+
position: absolute;
434+
top: 0;
435+
bottom: 0;
436+
left: 0;
437+
right: 0;
438+
}
402439
[dir=rtl] .sidebar { left: unset; right: 0; }
403440
.sidebar-resizing {
404441
-moz-user-select: none;
405442
-webkit-user-select: none;
406443
-ms-user-select: none;
407444
user-select: none;
408445
}
409-
.no-js .sidebar,
410-
.js:not(.sidebar-resizing) .sidebar {
446+
html:not(.sidebar-resizing) .sidebar {
411447
transition: transform 0.3s; /* Animation: slide away */
412448
}
413449
.sidebar code {

css/general.css

+10
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,16 @@ kbd {
190190
vertical-align: middle;
191191
}
192192

193+
sup {
194+
/* Set the line-height for superscript and footnote references so that there
195+
isn't an awkward space appearing above lines that contain the footnote.
196+
197+
See https://github.com/rust-lang/mdBook/pull/2443#discussion_r1813773583
198+
for an explanation.
199+
*/
200+
line-height: 0;
201+
}
202+
193203
:not(.footnote-definition) + .footnote-definition,
194204
.footnote-definition + :not(.footnote-definition) {
195205
margin-block-start: 2em;

css/variables.css

+33-3
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,11 @@
5656
--search-mark-bg: #e3b171;
5757

5858
--color-scheme: dark;
59+
60+
/* Same as `--icons` */
61+
--copy-button-filter: invert(45%) sepia(6%) saturate(621%) hue-rotate(198deg) brightness(99%) contrast(85%);
62+
/* Same as `--sidebar-active` */
63+
--copy-button-filter-hover: invert(68%) sepia(55%) saturate(531%) hue-rotate(341deg) brightness(104%) contrast(101%);
5964
}
6065

6166
.coal {
@@ -100,9 +105,14 @@
100105
--search-mark-bg: #355c7d;
101106

102107
--color-scheme: dark;
108+
109+
/* Same as `--icons` */
110+
--copy-button-filter: invert(26%) sepia(8%) saturate(575%) hue-rotate(169deg) brightness(87%) contrast(82%);
111+
/* Same as `--sidebar-active` */
112+
--copy-button-filter-hover: invert(36%) sepia(70%) saturate(503%) hue-rotate(167deg) brightness(98%) contrast(89%);
103113
}
104114

105-
.light {
115+
.light, html:not(.js) {
106116
--bg: hsl(0, 0%, 100%);
107117
--fg: hsl(0, 0%, 0%);
108118

@@ -144,6 +154,11 @@
144154
--search-mark-bg: #a2cff5;
145155

146156
--color-scheme: light;
157+
158+
/* Same as `--icons` */
159+
--copy-button-filter: invert(45.49%);
160+
/* Same as `--sidebar-active` */
161+
--copy-button-filter-hover: invert(14%) sepia(93%) saturate(4250%) hue-rotate(243deg) brightness(99%) contrast(130%);
147162
}
148163

149164
.navy {
@@ -188,6 +203,11 @@
188203
--search-mark-bg: #a2cff5;
189204

190205
--color-scheme: dark;
206+
207+
/* Same as `--icons` */
208+
--copy-button-filter: invert(51%) sepia(10%) saturate(393%) hue-rotate(198deg) brightness(86%) contrast(87%);
209+
/* Same as `--sidebar-active` */
210+
--copy-button-filter-hover: invert(46%) sepia(20%) saturate(1537%) hue-rotate(156deg) brightness(85%) contrast(90%);
191211
}
192212

193213
.rust {
@@ -231,11 +251,14 @@
231251
--searchresults-li-bg: #dec2a2;
232252
--search-mark-bg: #e69f67;
233253

234-
--color-scheme: light;
254+
/* Same as `--icons` */
255+
--copy-button-filter: invert(51%) sepia(10%) saturate(393%) hue-rotate(198deg) brightness(86%) contrast(87%);
256+
/* Same as `--sidebar-active` */
257+
--copy-button-filter-hover: invert(77%) sepia(16%) saturate(1798%) hue-rotate(328deg) brightness(98%) contrast(83%);
235258
}
236259

237260
@media (prefers-color-scheme: dark) {
238-
.light.no-js {
261+
html:not(.js) {
239262
--bg: hsl(200, 7%, 8%);
240263
--fg: #98a3ad;
241264

@@ -275,5 +298,12 @@
275298
--searchresults-border-color: #98a3ad;
276299
--searchresults-li-bg: #2b2b2f;
277300
--search-mark-bg: #355c7d;
301+
302+
--color-scheme: dark;
303+
304+
/* Same as `--icons` */
305+
--copy-button-filter: invert(26%) sepia(8%) saturate(575%) hue-rotate(169deg) brightness(87%) contrast(82%);
306+
/* Same as `--sidebar-active` */
307+
--copy-button-filter-hover: invert(36%) sepia(70%) saturate(503%) hue-rotate(167deg) brightness(98%) contrast(89%);
278308
}
279309
}

0 commit comments

Comments
 (0)