Skip to content

Commit ec7d0dd

Browse files
sylvestresylvestre
committed
deploy: 2ed80ff 
1 parent 9ab631d commit ec7d0dd

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

131 files changed

+1686
-1787
lines changed

‎user/404.html

+13-14
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@
3232
}
3333
</style>
3434

35-
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
3635
<meta name="description" content="">
3736
<meta name="viewport" content="width=device-width, initial-scale=1">
3837
<meta name="theme-color" content="#ffffff" />
@@ -57,13 +56,13 @@
5756
</head>
5857
<body>
5958
<!-- Provide site root to javascript -->
60-
<script type="text/javascript">
59+
<script>
6160
var path_to_root = "";
6261
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
6362
</script>
6463

6564
<!-- Work around some values being stored in localStorage wrapped in quotes -->
66-
<script type="text/javascript">
65+
<script>
6766
try {
6867
var theme = localStorage.getItem('mdbook-theme');
6968
var sidebar = localStorage.getItem('mdbook-sidebar');
@@ -79,7 +78,7 @@
7978
</script>
8079

8180
<!-- Set the theme before any content is loaded, prevents flash -->
82-
<script type="text/javascript">
81+
<script>
8382
var theme;
8483
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
8584
if (theme === null || theme === undefined) { theme = default_theme; }
@@ -91,7 +90,7 @@
9190
</script>
9291

9392
<!-- Hide / unhide sidebar before it is displayed -->
94-
<script type="text/javascript">
93+
<script>
9594
var html = document.querySelector('html');
9695
var sidebar = 'hidden';
9796
if (document.body.clientWidth >= 1080) {
@@ -122,7 +121,7 @@
122121
<i class="fa fa-paint-brush"></i>
123122
</button>
124123
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
125-
<li role="none"><button role="menuitem" class="theme" id="light">Light (default)</button></li>
124+
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
126125
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
127126
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
128127
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
@@ -158,7 +157,7 @@ <h1 class="menu-title">uutils Documentation</h1>
158157
</div>
159158

160159
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
161-
<script type="text/javascript">
160+
<script>
162161
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
163162
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
164163
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
@@ -191,18 +190,18 @@ <h1 id="document-not-found-404"><a class="header" href="#document-not-found-404"
191190

192191

193192

194-
<script type="text/javascript">
193+
<script>
195194
window.playground_copyable = true;
196195
</script>
197196

198197

199-
<script src="elasticlunr.min.js" type="text/javascript" charset="utf-8"></script>
200-
<script src="mark.min.js" type="text/javascript" charset="utf-8"></script>
201-
<script src="searcher.js" type="text/javascript" charset="utf-8"></script>
198+
<script src="elasticlunr.min.js"></script>
199+
<script src="mark.min.js"></script>
200+
<script src="searcher.js"></script>
202201

203-
<script src="clipboard.min.js" type="text/javascript" charset="utf-8"></script>
204-
<script src="highlight.js" type="text/javascript" charset="utf-8"></script>
205-
<script src="book.js" type="text/javascript" charset="utf-8"></script>
202+
<script src="clipboard.min.js"></script>
203+
<script src="highlight.js"></script>
204+
<script src="book.js"></script>
206205

207206
<!-- Custom JS scripts -->
208207

‎user/book.js

+9-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ function playground_text(playground) {
1111
let editor = window.ace.edit(code_block);
1212
return editor.getValue();
1313
} else {
14-
return code_block.textContent;
14+
return code_block.innerText;
1515
}
1616
}
1717

@@ -300,6 +300,13 @@ function playground_text(playground) {
300300
themePopup.querySelector("button#" + get_theme()).focus();
301301
}
302302

303+
function updateThemeSelected() {
304+
themePopup.querySelectorAll('.theme-selected').forEach(function (el) {
305+
el.classList.remove('theme-selected');
306+
});
307+
themePopup.querySelector("button#" + get_theme()).classList.add('theme-selected');
308+
}
309+
303310
function hideThemes() {
304311
themePopup.style.display = 'none';
305312
themeToggleButton.setAttribute('aria-expanded', false);
@@ -355,6 +362,7 @@ function playground_text(playground) {
355362

356363
html.classList.remove(previousTheme);
357364
html.classList.add(theme);
365+
updateThemeSelected();
358366
}
359367

360368
// Set theme

‎user/build.html

+13-14
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,6 @@
3131
}
3232
</style>
3333

34-
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
3534
<meta name="description" content="">
3635
<meta name="viewport" content="width=device-width, initial-scale=1">
3736
<meta name="theme-color" content="#ffffff" />
@@ -56,13 +55,13 @@
5655
</head>
5756
<body>
5857
<!-- Provide site root to javascript -->
59-
<script type="text/javascript">
58+
<script>
6059
var path_to_root = "";
6160
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
6261
</script>
6362

6463
<!-- Work around some values being stored in localStorage wrapped in quotes -->
65-
<script type="text/javascript">
64+
<script>
6665
try {
6766
var theme = localStorage.getItem('mdbook-theme');
6867
var sidebar = localStorage.getItem('mdbook-sidebar');
@@ -78,7 +77,7 @@
7877
</script>
7978

8079
<!-- Set the theme before any content is loaded, prevents flash -->
81-
<script type="text/javascript">
80+
<script>
8281
var theme;
8382
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
8483
if (theme === null || theme === undefined) { theme = default_theme; }
@@ -90,7 +89,7 @@
9089
</script>
9190

9291
<!-- Hide / unhide sidebar before it is displayed -->
93-
<script type="text/javascript">
92+
<script>
9493
var html = document.querySelector('html');
9594
var sidebar = 'hidden';
9695
if (document.body.clientWidth >= 1080) {
@@ -121,7 +120,7 @@
121120
<i class="fa fa-paint-brush"></i>
122121
</button>
123122
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
124-
<li role="none"><button role="menuitem" class="theme" id="light">Light (default)</button></li>
123+
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
125124
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
126125
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
127126
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
@@ -157,7 +156,7 @@ <h1 class="menu-title">uutils Documentation</h1>
157156
</div>
158157

159158
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
160-
<script type="text/javascript">
159+
<script>
161160
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
162161
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
163162
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
@@ -325,18 +324,18 @@ <h3 id="gnu-make-2"><a class="header" href="#gnu-make-2">GNU Make</a></h3>
325324

326325

327326

328-
<script type="text/javascript">
327+
<script>
329328
window.playground_copyable = true;
330329
</script>
331330

332331

333-
<script src="elasticlunr.min.js" type="text/javascript" charset="utf-8"></script>
334-
<script src="mark.min.js" type="text/javascript" charset="utf-8"></script>
335-
<script src="searcher.js" type="text/javascript" charset="utf-8"></script>
332+
<script src="elasticlunr.min.js"></script>
333+
<script src="mark.min.js"></script>
334+
<script src="searcher.js"></script>
336335

337-
<script src="clipboard.min.js" type="text/javascript" charset="utf-8"></script>
338-
<script src="highlight.js" type="text/javascript" charset="utf-8"></script>
339-
<script src="book.js" type="text/javascript" charset="utf-8"></script>
336+
<script src="clipboard.min.js"></script>
337+
<script src="highlight.js"></script>
338+
<script src="book.js"></script>
340339

341340
<!-- Custom JS scripts -->
342341

‎user/contributing.html

+13-14
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,6 @@
3131
}
3232
</style>
3333

34-
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
3534
<meta name="description" content="">
3635
<meta name="viewport" content="width=device-width, initial-scale=1">
3736
<meta name="theme-color" content="#ffffff" />
@@ -56,13 +55,13 @@
5655
</head>
5756
<body>
5857
<!-- Provide site root to javascript -->
59-
<script type="text/javascript">
58+
<script>
6059
var path_to_root = "";
6160
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
6261
</script>
6362

6463
<!-- Work around some values being stored in localStorage wrapped in quotes -->
65-
<script type="text/javascript">
64+
<script>
6665
try {
6766
var theme = localStorage.getItem('mdbook-theme');
6867
var sidebar = localStorage.getItem('mdbook-sidebar');
@@ -78,7 +77,7 @@
7877
</script>
7978

8079
<!-- Set the theme before any content is loaded, prevents flash -->
81-
<script type="text/javascript">
80+
<script>
8281
var theme;
8382
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
8483
if (theme === null || theme === undefined) { theme = default_theme; }
@@ -90,7 +89,7 @@
9089
</script>
9190

9291
<!-- Hide / unhide sidebar before it is displayed -->
93-
<script type="text/javascript">
92+
<script>
9493
var html = document.querySelector('html');
9594
var sidebar = 'hidden';
9695
if (document.body.clientWidth >= 1080) {
@@ -121,7 +120,7 @@
121120
<i class="fa fa-paint-brush"></i>
122121
</button>
123122
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
124-
<li role="none"><button role="menuitem" class="theme" id="light">Light (default)</button></li>
123+
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
125124
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
126125
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
127126
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
@@ -157,7 +156,7 @@ <h1 class="menu-title">uutils Documentation</h1>
157156
</div>
158157

159158
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
160-
<script type="text/javascript">
159+
<script>
161160
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
162161
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
163162
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
@@ -313,18 +312,18 @@ <h2 id="licensing"><a class="header" href="#licensing">Licensing</a></h2>
313312

314313

315314

316-
<script type="text/javascript">
315+
<script>
317316
window.playground_copyable = true;
318317
</script>
319318

320319

321-
<script src="elasticlunr.min.js" type="text/javascript" charset="utf-8"></script>
322-
<script src="mark.min.js" type="text/javascript" charset="utf-8"></script>
323-
<script src="searcher.js" type="text/javascript" charset="utf-8"></script>
320+
<script src="elasticlunr.min.js"></script>
321+
<script src="mark.min.js"></script>
322+
<script src="searcher.js"></script>
324323

325-
<script src="clipboard.min.js" type="text/javascript" charset="utf-8"></script>
326-
<script src="highlight.js" type="text/javascript" charset="utf-8"></script>
327-
<script src="book.js" type="text/javascript" charset="utf-8"></script>
324+
<script src="clipboard.min.js"></script>
325+
<script src="highlight.js"></script>
326+
<script src="book.js"></script>
328327

329328
<!-- Custom JS scripts -->
330329

‎user/css/chrome.css

+9-5
Original file line numberDiff line numberDiff line change
@@ -507,6 +507,8 @@ ul#searchresults span.teaser em {
507507
padding: 0;
508508
list-style: none;
509509
display: none;
510+
/* Don't let the children's background extend past the rounded corners. */
511+
overflow: hidden;
510512
}
511513
.theme-popup .default {
512514
color: var(--icons);
@@ -515,7 +517,7 @@ ul#searchresults span.teaser em {
515517
width: 100%;
516518
border: 0;
517519
margin: 0;
518-
padding: 2px 10px;
520+
padding: 2px 20px;
519521
line-height: 25px;
520522
white-space: nowrap;
521523
text-align: left;
@@ -527,8 +529,10 @@ ul#searchresults span.teaser em {
527529
.theme-popup .theme:hover {
528530
background-color: var(--theme-hover);
529531
}
530-
.theme-popup .theme:hover:first-child,
531-
.theme-popup .theme:hover:last-child {
532-
border-top-left-radius: inherit;
533-
border-top-right-radius: inherit;
532+
533+
.theme-selected::before {
534+
display: inline-block;
535+
content: "✓";
536+
margin-left: -14px;
537+
width: 14px;
534538
}

‎user/css/general.css

+14-2
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ body {
2222
}
2323

2424
code {
25-
font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important;
26-
font-size: 0.875em; /* please adjust the ace font size accordingly in editor.js */
25+
font-family: var(--mono-font) !important;
26+
font-size: var(--code-font-size);
2727
}
2828

2929
/* make long words/inline code not x overflow */
@@ -148,6 +148,18 @@ blockquote {
148148
border-bottom: .1em solid var(--quote-border);
149149
}
150150

151+
kbd {
152+
background-color: var(--table-border-color);
153+
border-radius: 4px;
154+
border: solid 1px var(--theme-popup-border);
155+
box-shadow: inset 0 -1px 0 var(--theme-hover);
156+
display: inline-block;
157+
font-size: var(--code-font-size);
158+
font-family: var(--mono-font);
159+
line-height: 10px;
160+
padding: 4px 5px;
161+
vertical-align: middle;
162+
}
151163

152164
:not(.footnote-definition) + .footnote-definition,
153165
.footnote-definition + :not(.footnote-definition) {

‎user/css/variables.css

+2
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@
66
--page-padding: 15px;
77
--content-max-width: 750px;
88
--menu-bar-height: 50px;
9+
--mono-font: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace;
10+
--code-font-size: 0.875em /* please adjust the ace font size accordingly in editor.js */
911
}
1012

1113
/* Themes */

0 commit comments

Comments
 (0)