2015-09-19 10:42:03 +01:00
|
|
|
/* See FiraSans-LICENSE.txt for the Fira Sans license. */
|
2014-04-12 21:39:12 +02:00
|
|
|
@font-face {
|
2016-11-06 21:03:08 +01:00
|
|
|
font-family: 'Fira Sans';
|
|
|
|
font-style: normal;
|
|
|
|
font-weight: 400;
|
2021-02-26 00:02:11 -08:00
|
|
|
src: local('Fira Sans'),
|
|
|
|
url("FiraSans-Regular.woff2") format("woff2"),
|
|
|
|
url("FiraSans-Regular.woff") format('woff');
|
2021-02-19 17:54:41 -08:00
|
|
|
font-display: swap;
|
2014-04-12 21:39:12 +02:00
|
|
|
}
|
|
|
|
@font-face {
|
2016-11-06 21:03:08 +01:00
|
|
|
font-family: 'Fira Sans';
|
|
|
|
font-style: normal;
|
|
|
|
font-weight: 500;
|
2021-02-26 00:02:11 -08:00
|
|
|
src: local('Fira Sans Medium'),
|
|
|
|
url("FiraSans-Medium.woff2") format("woff2"),
|
|
|
|
url("FiraSans-Medium.woff") format('woff');
|
2021-02-19 17:54:41 -08:00
|
|
|
font-display: swap;
|
2014-04-12 21:39:12 +02:00
|
|
|
}
|
2015-09-19 10:42:03 +01:00
|
|
|
|
2021-03-29 18:33:22 +02:00
|
|
|
/* See SourceSerif4-LICENSE.md for the Source Serif 4 license. */
|
2014-04-12 21:39:12 +02:00
|
|
|
@font-face {
|
2021-03-29 18:33:22 +02:00
|
|
|
font-family: 'Source Serif 4';
|
2016-11-06 21:03:08 +01:00
|
|
|
font-style: normal;
|
|
|
|
font-weight: 400;
|
2021-06-17 17:36:42 +02:00
|
|
|
src: local('Source Serif 4'),
|
|
|
|
url("SourceSerif4-Regular.ttf.woff2") format("woff2"),
|
|
|
|
url("SourceSerif4-Regular.ttf.woff") format("woff");
|
2021-02-19 17:54:41 -08:00
|
|
|
font-display: swap;
|
2014-04-12 21:39:12 +02:00
|
|
|
}
|
|
|
|
@font-face {
|
2021-03-29 18:33:22 +02:00
|
|
|
font-family: 'Source Serif 4';
|
2016-11-06 21:03:08 +01:00
|
|
|
font-style: italic;
|
|
|
|
font-weight: 400;
|
2021-06-17 17:36:42 +02:00
|
|
|
src: local('Source Serif 4 Italic'),
|
|
|
|
url("SourceSerif4-It.ttf.woff2") format("woff2"),
|
|
|
|
url("SourceSerif4-It.ttf.woff") format("woff");
|
2021-02-19 17:54:41 -08:00
|
|
|
font-display: swap;
|
2014-04-12 21:39:12 +02:00
|
|
|
}
|
|
|
|
@font-face {
|
2021-03-29 18:33:22 +02:00
|
|
|
font-family: 'Source Serif 4';
|
2016-11-06 21:03:08 +01:00
|
|
|
font-style: normal;
|
|
|
|
font-weight: 700;
|
2021-06-17 17:36:42 +02:00
|
|
|
src: local('Source Serif 4 Bold'),
|
|
|
|
url("SourceSerif4-Bold.ttf.woff2") format("woff2"),
|
|
|
|
url("SourceSerif4-Bold.ttf.woff") format("woff");
|
2021-02-19 17:54:41 -08:00
|
|
|
font-display: swap;
|
2014-04-12 21:39:12 +02:00
|
|
|
}
|
2015-09-19 10:42:03 +01:00
|
|
|
|
|
|
|
/* See SourceCodePro-LICENSE.txt for the Source Code Pro license. */
|
2014-07-08 20:26:23 +02:00
|
|
|
@font-face {
|
2016-11-06 21:03:08 +01:00
|
|
|
font-family: 'Source Code Pro';
|
|
|
|
font-style: normal;
|
|
|
|
font-weight: 400;
|
2016-12-04 13:44:19 -08:00
|
|
|
/* Avoid using locally installed font because bad versions are in circulation:
|
|
|
|
* see https://github.com/rust-lang/rust/issues/24355 */
|
2021-06-17 17:36:42 +02:00
|
|
|
src: url("SourceCodePro-Regular.ttf.woff2") format("woff2"),
|
|
|
|
url("SourceCodePro-Regular.ttf.woff") format("woff");
|
2021-03-04 15:38:31 +01:00
|
|
|
font-display: swap;
|
|
|
|
}
|
|
|
|
@font-face {
|
|
|
|
font-family: 'Source Code Pro';
|
|
|
|
font-style: italic;
|
|
|
|
font-weight: 400;
|
2021-06-17 17:36:42 +02:00
|
|
|
src: url("SourceCodePro-It.ttf.woff2") format("woff2"),
|
|
|
|
url("SourceCodePro-It.ttf.woff") format("woff");
|
2021-02-19 17:54:41 -08:00
|
|
|
font-display: swap;
|
2014-07-08 20:26:23 +02:00
|
|
|
}
|
|
|
|
@font-face {
|
2016-11-06 21:03:08 +01:00
|
|
|
font-family: 'Source Code Pro';
|
|
|
|
font-style: normal;
|
|
|
|
font-weight: 600;
|
2021-06-17 17:36:42 +02:00
|
|
|
src: url("SourceCodePro-Semibold.ttf.woff2") format("woff2"),
|
|
|
|
url("SourceCodePro-Semibold.ttf.woff") format("woff");
|
2021-02-19 17:54:41 -08:00
|
|
|
font-display: swap;
|
2014-07-08 20:26:23 +02:00
|
|
|
}
|
2014-04-12 21:39:12 +02:00
|
|
|
|
2021-10-12 04:47:34 +09:00
|
|
|
/* Avoid using legacy CJK serif fonts in Windows like Batang. */
|
2021-05-15 14:01:27 +09:00
|
|
|
@font-face {
|
2021-10-26 10:58:13 +09:00
|
|
|
font-family: 'NanumBarunGothic';
|
|
|
|
src: url("NanumBarunGothic.ttf.woff2") format("woff2"),
|
|
|
|
url("NanumBarunGothic.ttf.woff") format("woff");
|
2021-05-15 14:01:27 +09:00
|
|
|
font-display: swap;
|
2021-10-26 10:58:13 +09:00
|
|
|
unicode-range: U+AC00-D7AF, U+1100-11FF, U+3130-318F, U+A960-A97F, U+D7B0-D7FF;
|
2021-05-15 14:01:27 +09:00
|
|
|
}
|
|
|
|
|
2013-09-18 22:18:38 -07:00
|
|
|
* {
|
2020-07-15 17:20:46 +02:00
|
|
|
-webkit-box-sizing: border-box;
|
|
|
|
-moz-box-sizing: border-box;
|
|
|
|
box-sizing: border-box;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
|
2019-05-27 15:57:44 +02:00
|
|
|
/* This part handles the "default" theme being used depending on the system one. */
|
|
|
|
html {
|
|
|
|
content: "";
|
|
|
|
}
|
|
|
|
@media (prefers-color-scheme: light) {
|
|
|
|
html {
|
|
|
|
content: "light";
|
|
|
|
}
|
|
|
|
}
|
|
|
|
@media (prefers-color-scheme: dark) {
|
|
|
|
html {
|
|
|
|
content: "dark";
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2013-10-14 21:32:12 +02:00
|
|
|
/* General structure and fonts */
|
2013-09-18 22:18:38 -07:00
|
|
|
|
|
|
|
body {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font: 1rem/1.4 "Source Serif 4", NanumBarunGothic, serif;
|
2016-11-06 21:03:08 +01:00
|
|
|
margin: 0;
|
|
|
|
position: relative;
|
2022-01-11 17:36:52 -08:00
|
|
|
/* We use overflow-wrap: break-word for Safari, which doesn't recognize
|
|
|
|
`anywhere`: https://developer.mozilla.org/en-US/docs/Web/CSS/overflow-wrap */
|
|
|
|
overflow-wrap: break-word;
|
|
|
|
/* Then override it with `anywhere`, which is required to make non-Safari browsers break
|
|
|
|
more aggressively when we want them to. */
|
|
|
|
overflow-wrap: anywhere;
|
2014-11-01 00:16:48 +01:00
|
|
|
|
2016-11-06 21:03:08 +01:00
|
|
|
-webkit-font-feature-settings: "kern", "liga";
|
|
|
|
-moz-font-feature-settings: "kern", "liga";
|
|
|
|
font-feature-settings: "kern", "liga";
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
|
2014-04-27 09:07:12 +03:00
|
|
|
h1 {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.5rem;
|
2014-04-27 09:07:12 +03:00
|
|
|
}
|
|
|
|
h2 {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.4rem;
|
2014-04-27 09:07:12 +03:00
|
|
|
}
|
|
|
|
h3 {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.3rem;
|
2014-04-27 09:07:12 +03:00
|
|
|
}
|
2021-10-01 06:17:15 -04:00
|
|
|
h1, h2, h3, h4, h5, h6 {
|
2016-11-06 21:03:08 +01:00
|
|
|
font-weight: 500;
|
2021-10-18 21:04:38 -07:00
|
|
|
}
|
|
|
|
h1, h2, h3, h4 {
|
2016-11-06 21:03:08 +01:00
|
|
|
margin: 20px 0 15px 0;
|
|
|
|
padding-bottom: 6px;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
2021-10-21 23:09:11 -07:00
|
|
|
.docblock h3, .docblock h4, h5, h6 {
|
2021-10-18 21:04:38 -07:00
|
|
|
margin: 15px 0 5px 0;
|
|
|
|
}
|
2014-03-20 19:05:22 +01:00
|
|
|
h1.fqn {
|
2021-12-03 17:09:04 -08:00
|
|
|
margin: 0;
|
|
|
|
padding: 0;
|
|
|
|
}
|
|
|
|
.main-heading {
|
2021-04-20 22:31:48 +02:00
|
|
|
display: flex;
|
2021-12-03 17:09:04 -08:00
|
|
|
border-bottom: 1px dashed #DDDDDD;
|
|
|
|
padding-bottom: 6px;
|
|
|
|
margin-bottom: 15px;
|
2021-04-22 22:33:54 +02:00
|
|
|
|
|
|
|
/* workaround to keep flex from breaking below 700 px width due to the float: right on the nav
|
|
|
|
above the h1 */
|
|
|
|
padding-left: 1px;
|
2014-03-18 01:44:55 -06:00
|
|
|
}
|
2021-12-03 17:09:04 -08:00
|
|
|
.main-heading a:hover {
|
2020-07-05 11:56:41 -05:00
|
|
|
text-decoration: underline;
|
|
|
|
}
|
2021-12-03 17:09:04 -08:00
|
|
|
#toggle-all-docs {
|
|
|
|
text-decoration: none;
|
|
|
|
}
|
2021-10-21 23:09:11 -07:00
|
|
|
/* The only headings that get underlines are:
|
|
|
|
Markdown-generated headings within the top-doc
|
|
|
|
Rustdoc-generated h2 section headings (e.g. "Implementations", "Required Methods", etc)
|
|
|
|
Underlines elsewhere in the documentation break up visual flow and tend to invert
|
|
|
|
section hierarchies. */
|
|
|
|
h2,
|
|
|
|
.top-doc h3,
|
2021-11-04 16:27:02 +01:00
|
|
|
.top-doc h4,
|
|
|
|
.sidebar .others h3 {
|
2016-11-06 21:03:08 +01:00
|
|
|
border-bottom: 1px solid;
|
2014-03-18 01:44:55 -06:00
|
|
|
}
|
2021-10-21 18:46:47 -07:00
|
|
|
h3.code-header {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.1rem;
|
2021-10-21 18:46:47 -07:00
|
|
|
}
|
|
|
|
h4.code-header {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2021-10-21 18:46:47 -07:00
|
|
|
}
|
|
|
|
h3.code-header, h4.code-header {
|
2021-07-25 21:41:57 +00:00
|
|
|
font-weight: 600;
|
2021-10-21 18:46:47 -07:00
|
|
|
border-bottom-style: none;
|
2021-07-25 21:41:57 +00:00
|
|
|
padding: 0;
|
|
|
|
margin: 0;
|
|
|
|
}
|
2021-06-26 21:14:42 +02:00
|
|
|
.impl,
|
|
|
|
.impl-items .method,
|
|
|
|
.methods .method,
|
|
|
|
.impl-items .type,
|
|
|
|
.methods .type,
|
|
|
|
.impl-items .associatedconstant,
|
|
|
|
.methods .associatedconstant,
|
|
|
|
.impl-items .associatedtype,
|
|
|
|
.methods .associatedtype {
|
2018-12-26 21:23:05 -08:00
|
|
|
flex-basis: 100%;
|
2016-11-06 21:03:08 +01:00
|
|
|
font-weight: 600;
|
2018-12-26 21:23:05 -08:00
|
|
|
margin-top: 16px;
|
2016-11-06 21:03:08 +01:00
|
|
|
margin-bottom: 10px;
|
|
|
|
position: relative;
|
2014-04-18 11:08:34 +09:00
|
|
|
}
|
2017-10-01 15:54:50 +03:00
|
|
|
|
2021-04-23 22:15:57 +02:00
|
|
|
div.impl-items > div {
|
|
|
|
padding-left: 0;
|
|
|
|
}
|
|
|
|
|
2021-10-01 06:17:15 -04:00
|
|
|
h1, h2, h3, h4, h5, h6,
|
2021-05-09 12:56:21 -07:00
|
|
|
.sidebar, a.source, .search-input, .search-results .result-name,
|
2021-05-23 22:28:19 -07:00
|
|
|
.content table td:first-child > a,
|
2021-06-18 00:33:42 +02:00
|
|
|
.item-left > a,
|
2021-12-03 17:09:04 -08:00
|
|
|
.out-of-band,
|
|
|
|
span.since,
|
2020-12-29 15:56:52 +01:00
|
|
|
#source-sidebar, #sidebar-toggle,
|
2021-04-28 21:19:52 +02:00
|
|
|
details.rustdoc-toggle > summary::before,
|
2021-04-23 22:15:57 +02:00
|
|
|
div.impl-items > div:not(.docblock):not(.item-info),
|
2021-12-03 17:09:04 -08:00
|
|
|
.content ul.crate a.crate,
|
|
|
|
a.srclink,
|
2020-12-29 15:56:52 +01:00
|
|
|
/* This selector is for the items listed in the "all items" page. */
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content > ul.docblock > li > a {
|
2021-10-26 10:58:13 +09:00
|
|
|
font-family: "Fira Sans", Arial, NanumBarunGothic, sans-serif;
|
2014-04-12 21:39:12 +02:00
|
|
|
}
|
|
|
|
|
2020-09-07 13:54:31 -07:00
|
|
|
.content ul.crate a.crate {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem/1.6;
|
2020-09-07 13:54:31 -07:00
|
|
|
}
|
|
|
|
|
2014-04-18 11:08:34 +09:00
|
|
|
ol, ul {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding-left: 25px;
|
2014-04-12 21:39:12 +02:00
|
|
|
}
|
2014-04-18 11:08:34 +09:00
|
|
|
ul ul, ol ul, ul ol, ol ol {
|
2018-11-24 23:56:27 +00:00
|
|
|
margin-bottom: .6em;
|
2014-04-18 11:08:34 +09:00
|
|
|
}
|
2014-04-12 21:39:12 +02:00
|
|
|
|
|
|
|
p {
|
2016-11-06 21:03:08 +01:00
|
|
|
margin: 0 0 .6em 0;
|
2014-04-12 21:39:12 +02:00
|
|
|
}
|
2014-03-20 19:05:22 +01:00
|
|
|
|
2017-08-18 17:09:51 +02:00
|
|
|
summary {
|
|
|
|
outline: none;
|
|
|
|
}
|
|
|
|
|
2021-06-30 04:13:46 +09:00
|
|
|
/* Fix some style changes due to normalize.css 8 */
|
|
|
|
|
|
|
|
td,
|
|
|
|
th {
|
|
|
|
padding: 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
table {
|
|
|
|
border-collapse: collapse;
|
|
|
|
}
|
|
|
|
|
|
|
|
button,
|
|
|
|
input,
|
|
|
|
optgroup,
|
|
|
|
select,
|
|
|
|
textarea {
|
|
|
|
color: inherit;
|
|
|
|
font: inherit;
|
|
|
|
margin: 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
/* end tweaks for normalize.css 8 */
|
|
|
|
|
2021-09-30 04:23:02 +02:00
|
|
|
.rustdoc {
|
|
|
|
display: flex;
|
|
|
|
flex-direction: row;
|
|
|
|
flex-wrap: nowrap;
|
|
|
|
}
|
|
|
|
|
|
|
|
main {
|
|
|
|
position: relative;
|
|
|
|
flex-grow: 1;
|
|
|
|
padding: 10px 15px 40px 45px;
|
2021-10-24 20:03:13 +02:00
|
|
|
min-width: 0;
|
2021-09-30 04:23:02 +02:00
|
|
|
}
|
|
|
|
|
2021-10-10 00:52:14 +02:00
|
|
|
.source main {
|
|
|
|
padding: 15px;
|
|
|
|
}
|
|
|
|
|
2021-12-02 14:21:32 +01:00
|
|
|
.width-limiter {
|
2021-09-30 04:23:02 +02:00
|
|
|
max-width: 960px;
|
|
|
|
margin-right: auto;
|
|
|
|
}
|
|
|
|
|
2021-12-02 14:21:32 +01:00
|
|
|
.source .width-limiter {
|
2021-10-10 00:52:14 +02:00
|
|
|
max-width: unset;
|
|
|
|
}
|
|
|
|
|
2021-06-24 15:41:31 +09:00
|
|
|
details:not(.rustdoc-toggle) summary {
|
|
|
|
margin-bottom: .6em;
|
|
|
|
}
|
|
|
|
|
2021-07-25 21:41:57 +00:00
|
|
|
code, pre, a.test-arrow, .code-header {
|
2018-11-07 11:02:08 -05:00
|
|
|
font-family: "Source Code Pro", monospace;
|
2013-11-11 15:16:23 +01:00
|
|
|
}
|
2016-09-09 11:54:12 +08:00
|
|
|
.docblock code, .docblock-short code {
|
2016-11-06 21:03:08 +01:00
|
|
|
border-radius: 3px;
|
2018-09-19 22:59:35 +02:00
|
|
|
padding: 0 0.1em;
|
2014-08-06 11:03:18 +01:00
|
|
|
}
|
2021-04-01 13:31:55 -07:00
|
|
|
.docblock pre code, .docblock-short pre code {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: 0;
|
2015-07-12 19:42:42 -04:00
|
|
|
}
|
2013-11-11 15:16:23 +01:00
|
|
|
pre {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: 14px;
|
2014-04-25 17:34:32 +09:00
|
|
|
}
|
2021-10-18 14:49:25 +02:00
|
|
|
.docblock.item-decl {
|
|
|
|
margin-left: 0;
|
|
|
|
}
|
|
|
|
.item-decl pre {
|
2021-07-15 18:19:07 +02:00
|
|
|
overflow-x: auto;
|
|
|
|
}
|
2014-04-25 17:34:32 +09:00
|
|
|
|
2017-03-23 23:05:30 -04:00
|
|
|
.source .content pre {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: 20px;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
|
2016-01-02 21:38:36 -05:00
|
|
|
img {
|
2016-11-06 21:03:08 +01:00
|
|
|
max-width: 100%;
|
2016-01-02 21:38:36 -05:00
|
|
|
}
|
|
|
|
|
2019-06-29 18:28:39 +02:00
|
|
|
li {
|
|
|
|
position: relative;
|
|
|
|
}
|
|
|
|
|
2017-03-23 23:05:30 -04:00
|
|
|
.source .content {
|
2016-11-06 21:03:08 +01:00
|
|
|
max-width: none;
|
|
|
|
overflow: visible;
|
|
|
|
margin-left: 0px;
|
2014-07-28 22:33:43 -04:00
|
|
|
}
|
|
|
|
|
2013-09-18 22:18:38 -07:00
|
|
|
nav.sub {
|
2021-10-10 00:52:14 +02:00
|
|
|
position: relative;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2016-11-06 21:03:08 +01:00
|
|
|
text-transform: uppercase;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
|
2021-10-24 22:41:48 +02:00
|
|
|
.sub-container {
|
|
|
|
display: flex;
|
|
|
|
flex-direction: row;
|
|
|
|
flex-wrap: nowrap;
|
|
|
|
}
|
|
|
|
|
|
|
|
.sub-logo-container {
|
|
|
|
display: none;
|
|
|
|
margin-right: 20px;
|
|
|
|
}
|
|
|
|
|
|
|
|
.source .sub-logo-container {
|
|
|
|
display: block;
|
|
|
|
}
|
|
|
|
|
|
|
|
.source .sub-logo-container > img {
|
|
|
|
height: 60px;
|
|
|
|
width: 60px;
|
|
|
|
object-fit: contain;
|
|
|
|
}
|
|
|
|
|
2013-09-18 22:18:38 -07:00
|
|
|
.sidebar {
|
2016-11-06 21:03:08 +01:00
|
|
|
width: 200px;
|
2021-11-17 14:45:17 +01:00
|
|
|
overflow-y: scroll;
|
2021-10-24 20:03:13 +02:00
|
|
|
position: sticky;
|
|
|
|
min-width: 200px;
|
|
|
|
height: 100vh;
|
2021-11-29 15:55:05 +01:00
|
|
|
top: 0;
|
|
|
|
left: 0;
|
2020-04-07 22:10:17 +02:00
|
|
|
}
|
|
|
|
|
2021-11-25 17:08:23 +01:00
|
|
|
.rustdoc.source .sidebar {
|
2021-10-24 21:59:53 +02:00
|
|
|
width: 50px;
|
2021-10-10 19:08:08 +02:00
|
|
|
min-width: 0px;
|
|
|
|
max-width: 300px;
|
|
|
|
flex-grow: 0;
|
|
|
|
flex-shrink: 0;
|
|
|
|
flex-basis: auto;
|
|
|
|
border-right: 1px solid;
|
|
|
|
overflow-x: hidden;
|
2021-10-24 21:59:53 +02:00
|
|
|
/* The sidebar is by default hidden */
|
|
|
|
overflow-y: hidden;
|
|
|
|
}
|
|
|
|
|
|
|
|
.source .sidebar > *:not(:first-child) {
|
|
|
|
transition: opacity 0.5s, visibility 0.2s;
|
|
|
|
opacity: 0;
|
|
|
|
visibility: hidden;
|
|
|
|
}
|
|
|
|
|
|
|
|
.source .sidebar.expanded {
|
|
|
|
overflow-y: auto;
|
|
|
|
}
|
|
|
|
|
|
|
|
.source .sidebar.expanded > * {
|
|
|
|
opacity: 1;
|
|
|
|
visibility: visible;
|
2021-10-10 00:52:14 +02:00
|
|
|
}
|
|
|
|
|
2020-04-07 22:10:17 +02:00
|
|
|
/* Improve the scrollbar display on firefox */
|
|
|
|
* {
|
|
|
|
scrollbar-width: initial;
|
|
|
|
}
|
|
|
|
.sidebar {
|
2020-04-01 16:12:40 +02:00
|
|
|
scrollbar-width: thin;
|
|
|
|
}
|
|
|
|
|
2020-04-07 22:10:17 +02:00
|
|
|
/* Improve the scrollbar display on webkit-based browsers */
|
|
|
|
::-webkit-scrollbar {
|
|
|
|
width: 12px;
|
|
|
|
}
|
2020-04-01 16:12:40 +02:00
|
|
|
.sidebar::-webkit-scrollbar {
|
|
|
|
width: 8px;
|
|
|
|
}
|
2020-04-07 22:10:17 +02:00
|
|
|
::-webkit-scrollbar-track {
|
2020-04-01 16:12:40 +02:00
|
|
|
-webkit-box-shadow: inset 0;
|
2017-02-15 20:21:25 -05:00
|
|
|
}
|
|
|
|
|
2018-02-01 23:40:23 +01:00
|
|
|
.sidebar .block > ul > li {
|
2018-03-06 20:45:57 +01:00
|
|
|
margin-right: -10px;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
/* Everything else */
|
|
|
|
|
2019-11-11 16:54:45 +01:00
|
|
|
.hidden {
|
2018-02-01 23:40:23 +01:00
|
|
|
display: none !important;
|
|
|
|
}
|
2013-09-18 22:18:38 -07:00
|
|
|
|
2019-04-27 15:09:57 +02:00
|
|
|
.logo-container {
|
2021-10-24 21:59:53 +02:00
|
|
|
display: flex;
|
2017-10-10 23:39:10 +02:00
|
|
|
margin-top: 10px;
|
2021-10-24 21:59:53 +02:00
|
|
|
margin-bottom: 10px;
|
|
|
|
justify-content: center;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
|
2019-04-29 11:45:06 +02:00
|
|
|
.logo-container > img {
|
2021-10-24 21:59:53 +02:00
|
|
|
height: 100px;
|
|
|
|
width: 100px;
|
2019-04-29 11:45:06 +02:00
|
|
|
}
|
|
|
|
|
2014-03-18 01:44:55 -06:00
|
|
|
.sidebar .location {
|
2017-02-15 20:21:25 -05:00
|
|
|
border: 1px solid;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.0625rem;
|
2017-10-10 23:39:10 +02:00
|
|
|
margin: 30px 10px 20px 10px;
|
2016-11-06 21:03:08 +01:00
|
|
|
text-align: center;
|
2017-05-12 15:39:54 +02:00
|
|
|
word-wrap: break-word;
|
2021-07-16 21:58:23 -07:00
|
|
|
font-weight: inherit;
|
|
|
|
padding: 0;
|
2014-03-18 01:44:55 -06:00
|
|
|
}
|
|
|
|
|
2017-10-02 18:29:03 -05:00
|
|
|
.sidebar .version {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 0.9375rem;
|
2017-10-02 18:29:03 -05:00
|
|
|
text-align: center;
|
2017-12-02 13:19:29 +01:00
|
|
|
border-bottom: 1px solid;
|
2017-10-02 18:29:03 -05:00
|
|
|
overflow-wrap: break-word;
|
2022-01-11 17:36:52 -08:00
|
|
|
overflow-wrap: anywhere;
|
2017-10-02 18:29:03 -05:00
|
|
|
word-wrap: break-word; /* deprecated */
|
|
|
|
word-break: break-word; /* Chrome, non-standard */
|
|
|
|
}
|
|
|
|
|
2017-02-15 20:21:25 -05:00
|
|
|
.location:empty {
|
|
|
|
border: none;
|
|
|
|
}
|
|
|
|
|
2021-05-31 12:11:05 +02:00
|
|
|
.location a:first-of-type {
|
2018-02-01 23:40:23 +01:00
|
|
|
font-weight: 500;
|
|
|
|
}
|
2021-05-31 12:11:05 +02:00
|
|
|
.location a:hover {
|
|
|
|
text-decoration: underline;
|
|
|
|
}
|
2014-09-05 13:53:22 +08:00
|
|
|
|
2013-09-18 22:18:38 -07:00
|
|
|
.block {
|
2017-10-10 23:39:10 +02:00
|
|
|
padding: 0;
|
2016-11-06 21:03:08 +01:00
|
|
|
margin-bottom: 14px;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
2015-09-09 00:46:44 +09:00
|
|
|
.block h2, .block h3 {
|
2016-11-06 21:03:08 +01:00
|
|
|
text-align: center;
|
2014-03-18 01:44:55 -06:00
|
|
|
}
|
2015-09-09 00:46:44 +09:00
|
|
|
.block ul, .block li {
|
2017-10-10 23:39:10 +02:00
|
|
|
margin: 0 10px;
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: 0;
|
|
|
|
list-style: none;
|
2015-09-09 00:46:44 +09:00
|
|
|
}
|
2014-03-18 01:44:55 -06:00
|
|
|
|
2013-10-21 10:48:57 -07:00
|
|
|
.block a {
|
2016-11-06 21:03:08 +01:00
|
|
|
display: block;
|
|
|
|
text-overflow: ellipsis;
|
|
|
|
overflow: hidden;
|
|
|
|
line-height: 15px;
|
|
|
|
padding: 7px 5px;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 0.875rem;
|
2016-11-06 21:03:08 +01:00
|
|
|
font-weight: 300;
|
|
|
|
transition: border 500ms ease-out;
|
2014-03-18 01:44:55 -06:00
|
|
|
}
|
|
|
|
|
2017-10-10 23:39:10 +02:00
|
|
|
.sidebar-title {
|
2017-12-02 13:19:29 +01:00
|
|
|
border-top: 1px solid;
|
|
|
|
border-bottom: 1px solid;
|
2017-10-10 23:39:10 +02:00
|
|
|
text-align: center;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.0625rem;
|
2017-10-10 23:39:10 +02:00
|
|
|
margin-bottom: 5px;
|
2021-07-16 21:58:23 -07:00
|
|
|
font-weight: inherit;
|
|
|
|
padding: 0;
|
2017-10-10 23:39:10 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
.sidebar-links {
|
|
|
|
margin-bottom: 15px;
|
|
|
|
}
|
|
|
|
|
|
|
|
.sidebar-links > a {
|
|
|
|
padding-left: 10px;
|
|
|
|
width: 100%;
|
|
|
|
}
|
|
|
|
|
2017-12-06 00:42:33 +01:00
|
|
|
.sidebar-menu {
|
|
|
|
display: none;
|
|
|
|
}
|
|
|
|
|
2017-03-23 23:05:30 -04:00
|
|
|
.source .content pre.rust {
|
2016-11-06 21:03:08 +01:00
|
|
|
white-space: pre;
|
|
|
|
overflow: auto;
|
|
|
|
padding-left: 0;
|
2013-10-02 19:32:52 +02:00
|
|
|
}
|
2017-12-04 22:11:21 +01:00
|
|
|
|
2021-05-10 11:39:53 +02:00
|
|
|
.rustdoc .example-wrap {
|
2018-10-08 22:51:37 +02:00
|
|
|
display: inline-flex;
|
2018-11-10 21:58:47 +01:00
|
|
|
margin-bottom: 10px;
|
2018-10-29 22:38:26 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
.example-wrap {
|
2021-03-10 16:40:27 +01:00
|
|
|
position: relative;
|
2018-10-08 22:51:37 +02:00
|
|
|
width: 100%;
|
|
|
|
}
|
|
|
|
|
|
|
|
.example-wrap > pre.line-number {
|
|
|
|
overflow: initial;
|
|
|
|
border: 1px solid;
|
|
|
|
padding: 13px 8px;
|
|
|
|
text-align: right;
|
2021-05-11 11:16:14 +02:00
|
|
|
border-top-left-radius: 5px;
|
|
|
|
border-bottom-left-radius: 5px;
|
2018-10-08 22:51:37 +02:00
|
|
|
}
|
|
|
|
|
2021-04-14 13:26:49 +02:00
|
|
|
.example-wrap > pre.rust a:hover {
|
|
|
|
text-decoration: underline;
|
|
|
|
}
|
|
|
|
|
2021-07-11 12:40:31 +02:00
|
|
|
.rustdoc:not(.source) .example-wrap > pre:not(.line-number) {
|
2018-10-08 22:51:37 +02:00
|
|
|
width: 100%;
|
2018-12-02 19:12:37 +01:00
|
|
|
overflow-x: auto;
|
2018-10-08 22:51:37 +02:00
|
|
|
}
|
|
|
|
|
2021-10-19 20:08:30 -07:00
|
|
|
.rustdoc:not(.source) .example-wrap > pre.line-numbers {
|
|
|
|
width: auto;
|
|
|
|
overflow-x: visible;
|
|
|
|
}
|
|
|
|
|
2021-05-10 11:39:53 +02:00
|
|
|
.rustdoc .example-wrap > pre {
|
2018-11-10 21:58:47 +01:00
|
|
|
margin: 0;
|
|
|
|
}
|
|
|
|
|
2017-05-11 22:28:13 +02:00
|
|
|
#search {
|
2017-12-04 22:11:21 +01:00
|
|
|
position: relative;
|
2017-05-11 22:28:13 +02:00
|
|
|
}
|
2017-12-04 22:11:21 +01:00
|
|
|
|
2022-01-06 13:08:57 +01:00
|
|
|
.search-loading {
|
|
|
|
text-align: center;
|
|
|
|
}
|
|
|
|
|
2018-03-27 10:33:31 +02:00
|
|
|
#results > table {
|
|
|
|
width: 100%;
|
|
|
|
table-layout: fixed;
|
|
|
|
}
|
|
|
|
|
2021-05-10 11:39:53 +02:00
|
|
|
.content > .example-wrap pre.line-numbers {
|
2016-11-06 21:03:08 +01:00
|
|
|
position: relative;
|
|
|
|
-webkit-user-select: none;
|
|
|
|
-moz-user-select: none;
|
|
|
|
-ms-user-select: none;
|
|
|
|
user-select: none;
|
2014-12-20 03:56:47 +09:00
|
|
|
}
|
2018-02-01 23:40:23 +01:00
|
|
|
.line-numbers span {
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
2013-09-18 22:18:38 -07:00
|
|
|
|
2020-10-08 13:25:36 +02:00
|
|
|
.docblock-short {
|
2022-01-11 17:36:52 -08:00
|
|
|
overflow-wrap: break-word;
|
2020-10-08 13:25:36 +02:00
|
|
|
overflow-wrap: anywhere;
|
|
|
|
}
|
2016-09-06 15:59:16 +08:00
|
|
|
.docblock-short p {
|
2016-11-06 21:03:08 +01:00
|
|
|
display: inline;
|
2015-04-13 11:55:00 -07:00
|
|
|
}
|
|
|
|
|
2016-09-06 15:59:16 +08:00
|
|
|
.docblock-short p {
|
2016-11-06 21:03:08 +01:00
|
|
|
overflow: hidden;
|
|
|
|
text-overflow: ellipsis;
|
|
|
|
margin: 0;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
2021-03-29 21:49:58 +08:00
|
|
|
/* Wrap non-pre code blocks (`text`) but not (```text```). */
|
|
|
|
.docblock > :not(pre) > code,
|
|
|
|
.docblock-short > :not(pre) > code {
|
2021-01-31 01:27:21 +08:00
|
|
|
white-space: pre-wrap;
|
|
|
|
}
|
2013-09-18 22:18:38 -07:00
|
|
|
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
.top-doc .docblock h2 { font-size: 1.3rem; }
|
|
|
|
.top-doc .docblock h3 { font-size: 1.15rem; }
|
2021-05-16 20:47:03 -07:00
|
|
|
.top-doc .docblock h4,
|
2021-10-18 21:04:38 -07:00
|
|
|
.top-doc .docblock h5 {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.1rem;
|
2021-10-18 21:04:38 -07:00
|
|
|
}
|
2021-10-01 06:17:15 -04:00
|
|
|
.top-doc .docblock h6 {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2021-05-16 20:47:03 -07:00
|
|
|
}
|
2017-08-01 17:08:33 -05:00
|
|
|
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
.docblock h5 { font-size: 1rem; }
|
|
|
|
.docblock h6 { font-size: 0.95rem; }
|
2013-09-18 22:18:38 -07:00
|
|
|
|
2016-05-27 12:04:56 +02:00
|
|
|
.docblock {
|
2016-11-06 21:03:08 +01:00
|
|
|
margin-left: 24px;
|
2017-09-17 22:11:37 +02:00
|
|
|
position: relative;
|
2016-05-27 12:04:56 +02:00
|
|
|
}
|
|
|
|
|
2021-10-24 15:28:58 +02:00
|
|
|
.docblock > :not(.information) {
|
2021-09-08 15:08:11 +02:00
|
|
|
max-width: 100%;
|
|
|
|
overflow-x: auto;
|
|
|
|
}
|
|
|
|
|
2014-07-04 00:51:46 -07:00
|
|
|
.content .out-of-band {
|
2021-04-22 22:33:54 +02:00
|
|
|
flex-grow: 0;
|
|
|
|
text-align: right;
|
2021-12-03 17:09:04 -08:00
|
|
|
margin-left: auto;
|
|
|
|
margin-right: 0;
|
|
|
|
font-size: 1.15rem;
|
2021-04-22 22:33:54 +02:00
|
|
|
padding: 0 0 0 12px;
|
2016-11-06 21:03:08 +01:00
|
|
|
font-weight: normal;
|
2021-12-03 17:09:04 -08:00
|
|
|
float: right;
|
2016-05-05 04:46:45 +02:00
|
|
|
}
|
|
|
|
|
2021-07-25 21:41:57 +00:00
|
|
|
.method > .code-header, .trait-impl > .code-header, .invisible > .code-header {
|
2018-01-20 21:12:00 +01:00
|
|
|
max-width: calc(100% - 41px);
|
|
|
|
display: block;
|
2016-05-06 18:47:12 +02:00
|
|
|
}
|
|
|
|
|
2016-08-16 10:27:07 +12:00
|
|
|
.invisible {
|
2016-11-06 21:03:08 +01:00
|
|
|
width: 100%;
|
|
|
|
display: inline-block;
|
2016-08-16 10:27:07 +12:00
|
|
|
}
|
|
|
|
|
2014-08-02 20:58:41 -04:00
|
|
|
.content .in-band {
|
2021-04-22 22:33:54 +02:00
|
|
|
flex-grow: 1;
|
2016-11-06 21:03:08 +01:00
|
|
|
margin: 0px;
|
|
|
|
padding: 0px;
|
2022-01-11 17:36:52 -08:00
|
|
|
overflow-wrap: break-word;
|
2021-10-18 15:30:03 +02:00
|
|
|
overflow-wrap: anywhere;
|
2014-03-18 01:44:55 -06:00
|
|
|
}
|
|
|
|
|
2021-07-25 21:41:57 +00:00
|
|
|
.in-band > code, .in-band > .code-header {
|
2017-08-28 22:40:09 +02:00
|
|
|
display: inline-block;
|
|
|
|
}
|
|
|
|
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content {
|
2018-02-01 23:40:23 +01:00
|
|
|
position: relative;
|
|
|
|
}
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content > .since {
|
2016-11-06 21:03:08 +01:00
|
|
|
top: inherit;
|
2021-03-15 19:20:15 +02:00
|
|
|
font-family: "Fira Sans", Arial, sans-serif;
|
2016-05-06 18:47:12 +02:00
|
|
|
}
|
|
|
|
|
2018-03-28 09:00:58 +02:00
|
|
|
.content table:not(.table-display) {
|
2016-11-06 21:03:08 +01:00
|
|
|
border-spacing: 0 5px;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
.content td { vertical-align: top; }
|
|
|
|
.content td:first-child { padding-right: 20px; }
|
|
|
|
.content td p:first-child { margin-top: 0; }
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
.content td h1, .content td h2 { margin-left: 0; font-size: 1.1rem; }
|
2018-06-10 23:33:37 +02:00
|
|
|
.content tr:first-child td { border-top: 0; }
|
2013-09-18 22:18:38 -07:00
|
|
|
|
2015-02-15 15:58:45 +02:00
|
|
|
.docblock table {
|
2016-11-06 21:03:08 +01:00
|
|
|
margin: .5em 0;
|
2019-02-11 22:22:56 +01:00
|
|
|
width: calc(100% - 2px);
|
2021-07-17 23:39:18 +02:00
|
|
|
overflow-x: auto;
|
2022-01-11 17:36:52 -08:00
|
|
|
overflow-wrap: normal;
|
2021-07-17 23:39:18 +02:00
|
|
|
display: block;
|
2015-02-15 15:58:45 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
.docblock table td {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: .5em;
|
2018-06-10 23:33:37 +02:00
|
|
|
border: 1px dashed;
|
2015-02-15 15:58:45 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
.docblock table th {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: .5em;
|
|
|
|
text-align: left;
|
2018-06-10 23:33:37 +02:00
|
|
|
border: 1px solid;
|
2015-02-15 15:58:45 +02:00
|
|
|
}
|
|
|
|
|
2016-11-11 16:41:00 -06:00
|
|
|
.fields + table {
|
|
|
|
margin-bottom: 1em;
|
|
|
|
}
|
|
|
|
|
2013-09-18 22:18:38 -07:00
|
|
|
.content .item-list {
|
2016-11-06 21:03:08 +01:00
|
|
|
list-style-type: none;
|
|
|
|
padding: 0;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
.content .multi-column {
|
2016-11-06 21:03:08 +01:00
|
|
|
-moz-column-count: 5;
|
|
|
|
-moz-column-gap: 2.5em;
|
|
|
|
-webkit-column-count: 5;
|
|
|
|
-webkit-column-gap: 2.5em;
|
|
|
|
column-count: 5;
|
|
|
|
column-gap: 2.5em;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
.content .multi-column li { width: 100%; display: inline-block; }
|
|
|
|
|
2021-06-01 21:43:09 -07:00
|
|
|
.content > .methods > .method {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2016-11-06 21:03:08 +01:00
|
|
|
position: relative;
|
2014-07-30 21:31:34 -04:00
|
|
|
}
|
2015-05-31 22:46:19 +02:00
|
|
|
/* Shift "where ..." part of method or fn definition down a line */
|
2016-10-15 10:29:47 -05:00
|
|
|
.content .method .where,
|
|
|
|
.content .fn .where,
|
|
|
|
.content .where.fmt-newline {
|
2017-03-09 19:02:59 +01:00
|
|
|
display: block;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 0.8rem;
|
2016-10-15 10:29:47 -05:00
|
|
|
}
|
2014-12-27 22:45:13 -05:00
|
|
|
|
2021-04-23 22:15:57 +02:00
|
|
|
.content .methods > div:not(.notable-traits):not(.method) {
|
2018-03-28 10:48:00 +02:00
|
|
|
margin-left: 40px;
|
|
|
|
margin-bottom: 15px;
|
|
|
|
}
|
2014-06-26 11:37:39 -07:00
|
|
|
|
2018-05-30 01:10:48 +02:00
|
|
|
.content .docblock > .impl-items {
|
2016-11-06 21:03:08 +01:00
|
|
|
margin-left: 20px;
|
2018-05-30 01:10:48 +02:00
|
|
|
margin-top: -34px;
|
|
|
|
}
|
|
|
|
.content .docblock >.impl-items .table-display {
|
|
|
|
margin: 0;
|
|
|
|
}
|
|
|
|
.content .docblock >.impl-items table td {
|
|
|
|
padding: 0;
|
|
|
|
}
|
|
|
|
.content .docblock > .impl-items .table-display, .impl-items table td {
|
|
|
|
border: none;
|
2015-04-13 11:55:00 -07:00
|
|
|
}
|
2013-09-18 22:18:38 -07:00
|
|
|
|
2020-11-23 13:20:16 +01:00
|
|
|
.content .item-info code {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 0.81rem;
|
2015-08-17 20:23:47 +02:00
|
|
|
}
|
|
|
|
|
2020-11-23 13:20:16 +01:00
|
|
|
.content .item-info {
|
2018-08-04 00:02:46 +02:00
|
|
|
position: relative;
|
|
|
|
margin-left: 33px;
|
|
|
|
}
|
2018-08-27 21:52:10 +02:00
|
|
|
|
2020-11-23 13:20:16 +01:00
|
|
|
.sub-variant > div > .item-info {
|
2018-10-19 01:34:46 +02:00
|
|
|
margin-top: initial;
|
|
|
|
}
|
|
|
|
|
2020-11-23 13:20:16 +01:00
|
|
|
.content .item-info::before {
|
2020-01-09 09:54:05 +08:00
|
|
|
content: '⬑';
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.5625rem;
|
2018-08-04 00:02:46 +02:00
|
|
|
position: absolute;
|
2020-01-07 10:25:02 +08:00
|
|
|
top: -6px;
|
2020-01-09 09:54:05 +08:00
|
|
|
left: -19px;
|
2018-08-04 00:02:46 +02:00
|
|
|
}
|
2018-09-12 22:18:00 +02:00
|
|
|
|
2020-11-23 13:20:16 +01:00
|
|
|
.content .impl-items .docblock, .content .impl-items .item-info {
|
2018-09-12 22:18:00 +02:00
|
|
|
margin-bottom: .6em;
|
|
|
|
}
|
|
|
|
|
2020-11-23 13:20:16 +01:00
|
|
|
.content .impl-items > .item-info {
|
2018-09-12 22:18:00 +02:00
|
|
|
margin-left: 40px;
|
|
|
|
}
|
|
|
|
|
2020-11-23 13:20:16 +01:00
|
|
|
.methods > .item-info, .content .impl-items > .item-info {
|
2018-08-29 22:48:37 +02:00
|
|
|
margin-top: -8px;
|
|
|
|
}
|
2018-08-04 00:02:46 +02:00
|
|
|
|
2018-12-26 21:23:05 -08:00
|
|
|
.impl-items {
|
|
|
|
flex-basis: 100%;
|
|
|
|
}
|
|
|
|
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content > .item-info {
|
2018-08-27 21:52:10 +02:00
|
|
|
margin-top: 0;
|
|
|
|
}
|
|
|
|
|
2019-10-01 10:32:45 +02:00
|
|
|
nav:not(.sidebar) {
|
2021-10-24 22:41:48 +02:00
|
|
|
flex-grow: 1;
|
2016-11-06 21:03:08 +01:00
|
|
|
border-bottom: 1px solid;
|
|
|
|
padding-bottom: 10px;
|
2021-09-30 04:23:02 +02:00
|
|
|
margin-bottom: 25px;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
2021-10-10 00:52:14 +02:00
|
|
|
.source nav:not(.sidebar).sub {
|
2021-10-10 19:08:08 +02:00
|
|
|
margin-left: 32px;
|
2021-10-10 00:52:14 +02:00
|
|
|
}
|
2013-09-18 22:18:38 -07:00
|
|
|
nav.main {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: 20px 0;
|
|
|
|
text-align: center;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
nav.main .current {
|
2016-11-06 21:03:08 +01:00
|
|
|
border-top: 1px solid;
|
|
|
|
border-bottom: 1px solid;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
nav.main .separator {
|
2016-11-06 21:03:08 +01:00
|
|
|
border: 1px solid;
|
|
|
|
display: inline-block;
|
|
|
|
height: 23px;
|
|
|
|
margin: 0 20px;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
nav.sum { text-align: right; }
|
|
|
|
nav.sub form { display: inline; }
|
|
|
|
|
|
|
|
a {
|
2016-11-06 21:03:08 +01:00
|
|
|
text-decoration: none;
|
|
|
|
background: transparent;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
2015-02-20 13:54:11 +02:00
|
|
|
|
2021-06-17 09:57:48 +02:00
|
|
|
.small-section-header {
|
|
|
|
display: flex;
|
|
|
|
justify-content: space-between;
|
|
|
|
position: relative;
|
|
|
|
}
|
|
|
|
|
2017-08-08 22:16:08 +02:00
|
|
|
.small-section-header:hover > .anchor {
|
|
|
|
display: initial;
|
|
|
|
}
|
2017-08-18 09:38:52 -07:00
|
|
|
|
2021-03-11 03:32:30 +01:00
|
|
|
.in-band:hover > .anchor, .impl:hover > .anchor, .method.trait-impl:hover > .anchor,
|
2021-04-30 16:50:03 +02:00
|
|
|
.type.trait-impl:hover > .anchor, .associatedconstant.trait-impl:hover > .anchor,
|
|
|
|
.associatedtype.trait-impl:hover > .anchor {
|
2017-08-28 22:40:09 +02:00
|
|
|
display: inline-block;
|
|
|
|
position: absolute;
|
2017-08-18 09:38:52 -07:00
|
|
|
}
|
2017-08-08 22:16:08 +02:00
|
|
|
.anchor {
|
|
|
|
display: none;
|
2017-09-17 22:11:37 +02:00
|
|
|
position: absolute;
|
2021-10-21 18:46:47 -07:00
|
|
|
left: -0.5em;
|
2021-08-06 16:47:35 +02:00
|
|
|
background: none !important;
|
2017-08-08 22:16:08 +02:00
|
|
|
}
|
2017-09-17 22:11:37 +02:00
|
|
|
.anchor.field {
|
2018-02-17 20:46:06 +03:00
|
|
|
left: -5px;
|
2017-09-17 22:11:37 +02:00
|
|
|
}
|
2018-03-06 22:05:41 +01:00
|
|
|
.small-section-header > .anchor {
|
2021-08-06 16:47:35 +02:00
|
|
|
left: -15px;
|
|
|
|
padding-right: 8px;
|
|
|
|
}
|
|
|
|
h2.small-section-header > .anchor {
|
|
|
|
padding-right: 6px;
|
2018-03-06 22:05:41 +01:00
|
|
|
}
|
2021-08-06 16:47:35 +02:00
|
|
|
.anchor::before {
|
|
|
|
content: '§';
|
2017-08-08 22:16:08 +02:00
|
|
|
}
|
|
|
|
|
2018-06-02 13:47:42 +02:00
|
|
|
.docblock a:not(.srclink):not(.test-arrow):hover,
|
2020-11-23 13:20:16 +01:00
|
|
|
.docblock-short a:not(.srclink):not(.test-arrow):hover, .item-info a {
|
2016-11-06 21:03:08 +01:00
|
|
|
text-decoration: underline;
|
2015-02-20 13:54:11 +02:00
|
|
|
}
|
2013-09-18 22:18:38 -07:00
|
|
|
|
2021-04-23 22:15:57 +02:00
|
|
|
.invisible > .srclink,
|
2021-07-25 21:41:57 +00:00
|
|
|
.method > .code-header + .srclink {
|
2018-08-16 00:46:38 +02:00
|
|
|
position: absolute;
|
|
|
|
top: 0;
|
|
|
|
right: 0;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.0625rem;
|
2018-08-16 00:46:38 +02:00
|
|
|
font-weight: normal;
|
|
|
|
}
|
|
|
|
|
2015-09-09 00:46:44 +09:00
|
|
|
.block a.current.crate { font-weight: 500; }
|
2013-09-18 22:18:38 -07:00
|
|
|
|
2021-06-18 00:33:42 +02:00
|
|
|
.item-table {
|
2021-10-11 00:38:56 +02:00
|
|
|
display: table;
|
2021-05-25 00:36:36 +02:00
|
|
|
}
|
2021-09-12 01:18:39 +02:00
|
|
|
.item-row {
|
|
|
|
display: table-row;
|
|
|
|
}
|
2021-06-18 00:33:42 +02:00
|
|
|
.item-left, .item-right {
|
2021-09-12 01:18:39 +02:00
|
|
|
display: table-cell;
|
2021-05-25 00:36:36 +02:00
|
|
|
}
|
2021-06-18 00:33:42 +02:00
|
|
|
.item-left {
|
2021-09-12 01:18:39 +02:00
|
|
|
padding-right: 1.2rem;
|
2021-05-25 00:36:36 +02:00
|
|
|
}
|
|
|
|
|
2018-04-13 22:54:09 +02:00
|
|
|
.search-container {
|
|
|
|
position: relative;
|
2021-10-10 00:52:14 +02:00
|
|
|
max-width: 960px;
|
2018-04-13 22:54:09 +02:00
|
|
|
}
|
2018-10-01 00:47:54 +02:00
|
|
|
.search-container > div {
|
|
|
|
display: inline-flex;
|
2020-08-10 16:42:11 +02:00
|
|
|
width: calc(100% - 63px);
|
2018-10-01 00:47:54 +02:00
|
|
|
}
|
2022-01-01 23:48:34 -05:00
|
|
|
.search-results-title {
|
|
|
|
display: inline;
|
|
|
|
}
|
|
|
|
#search-settings {
|
|
|
|
font-size: 1.5rem;
|
|
|
|
font-weight: 500;
|
|
|
|
margin-bottom: 20px;
|
|
|
|
}
|
2018-10-01 00:47:54 +02:00
|
|
|
#crate-search {
|
2021-02-19 17:54:41 -08:00
|
|
|
min-width: 115px;
|
2018-10-01 00:47:54 +02:00
|
|
|
margin-top: 5px;
|
2022-01-01 23:48:34 -05:00
|
|
|
margin-left: 0.2em;
|
|
|
|
padding-left: 0.3em;
|
|
|
|
padding-right: 23px;
|
2018-10-01 00:47:54 +02:00
|
|
|
border: 0;
|
2022-01-01 23:48:34 -05:00
|
|
|
border-radius: 4px;
|
2018-10-01 00:47:54 +02:00
|
|
|
outline: none;
|
|
|
|
cursor: pointer;
|
|
|
|
-moz-appearance: none;
|
|
|
|
-webkit-appearance: none;
|
|
|
|
/* Removes default arrow from firefox */
|
|
|
|
text-indent: 0.01px;
|
|
|
|
text-overflow: "";
|
2018-11-29 01:29:49 +01:00
|
|
|
background-repeat: no-repeat;
|
|
|
|
background-color: transparent;
|
2018-12-08 16:35:51 +01:00
|
|
|
background-size: 20px;
|
2018-11-29 01:29:49 +01:00
|
|
|
background-position: calc(100% - 1px) 56%;
|
2021-11-23 21:23:54 -08:00
|
|
|
background-image: /* AUTOREPLACE: */url("down-arrow.svg");
|
2018-10-01 00:47:54 +02:00
|
|
|
}
|
2018-04-13 22:54:09 +02:00
|
|
|
.search-container > .top-button {
|
|
|
|
position: absolute;
|
|
|
|
right: 0;
|
|
|
|
top: 10px;
|
|
|
|
}
|
2013-09-18 22:18:38 -07:00
|
|
|
.search-input {
|
2021-12-08 23:39:42 -08:00
|
|
|
/* Override Normalize.css: it has a rule that sets
|
|
|
|
-webkit-appearance: textfield for search inputs. That
|
|
|
|
causes rounded corners and no border on iOS Safari. */
|
|
|
|
-webkit-appearance: none;
|
2016-11-06 21:03:08 +01:00
|
|
|
/* Override Normalize.css: we have margins and do
|
|
|
|
not want to overflow - the `moz` attribute is necessary
|
|
|
|
until Firefox 29, too early to drop at this point */
|
|
|
|
-moz-box-sizing: border-box !important;
|
|
|
|
box-sizing: border-box !important;
|
|
|
|
outline: none;
|
|
|
|
border: none;
|
2018-12-20 13:28:55 +01:00
|
|
|
border-radius: 1px;
|
2016-11-06 21:03:08 +01:00
|
|
|
margin-top: 5px;
|
|
|
|
padding: 10px 16px;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.0625rem;
|
2016-11-06 21:03:08 +01:00
|
|
|
transition: border-color 300ms ease;
|
|
|
|
transition: border-radius 300ms ease-in-out;
|
|
|
|
transition: box-shadow 300ms ease-in-out;
|
2019-05-02 23:31:50 +02:00
|
|
|
width: 100%;
|
2014-03-18 01:44:55 -06:00
|
|
|
}
|
|
|
|
|
|
|
|
.search-input:focus {
|
2016-11-06 21:03:08 +01:00
|
|
|
border-radius: 2px;
|
|
|
|
border: 0;
|
|
|
|
outline: 0;
|
2013-10-14 21:32:12 +02:00
|
|
|
}
|
2014-03-18 01:44:55 -06:00
|
|
|
|
2021-05-09 12:56:21 -07:00
|
|
|
.search-results {
|
|
|
|
display: none;
|
|
|
|
padding-bottom: 2em;
|
|
|
|
}
|
|
|
|
|
|
|
|
.search-results.active {
|
|
|
|
display: block;
|
2021-05-21 23:11:06 +02:00
|
|
|
/* prevent overhanging tabs from moving the first result */
|
|
|
|
clear: both;
|
2021-05-09 12:56:21 -07:00
|
|
|
}
|
|
|
|
|
2021-05-22 16:05:20 +02:00
|
|
|
.search-results .desc > span {
|
2016-11-06 21:03:08 +01:00
|
|
|
white-space: nowrap;
|
|
|
|
text-overflow: ellipsis;
|
|
|
|
overflow: hidden;
|
|
|
|
display: block;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
|
2021-05-21 16:39:03 +02:00
|
|
|
.search-results > a {
|
2021-05-21 23:11:06 +02:00
|
|
|
display: block;
|
2021-05-22 09:01:33 +00:00
|
|
|
width: 100%;
|
2021-05-09 12:56:21 -07:00
|
|
|
/* A little margin ensures the browser's outlining of focused links has room to display. */
|
|
|
|
margin-left: 2px;
|
|
|
|
margin-right: 2px;
|
2021-05-21 23:11:06 +02:00
|
|
|
border-bottom: 1px solid #aaa3;
|
2014-08-31 17:11:42 -04:00
|
|
|
}
|
|
|
|
|
2021-05-21 16:39:03 +02:00
|
|
|
.search-results > a > div {
|
|
|
|
display: flex;
|
2021-05-21 23:11:06 +02:00
|
|
|
flex-flow: row wrap;
|
2014-08-31 17:11:42 -04:00
|
|
|
}
|
|
|
|
|
2021-05-22 16:05:20 +02:00
|
|
|
.search-results .result-name, .search-results div.desc, .search-results .result-description {
|
2018-08-03 20:39:58 -04:00
|
|
|
width: 50%;
|
2021-05-21 16:39:03 +02:00
|
|
|
}
|
2021-05-21 23:54:49 +02:00
|
|
|
.search-results .result-name {
|
2021-05-21 23:11:06 +02:00
|
|
|
padding-right: 1em;
|
2021-05-21 16:39:03 +02:00
|
|
|
}
|
|
|
|
|
2021-05-21 23:54:49 +02:00
|
|
|
.search-results .result-name > span {
|
2021-05-21 16:39:03 +02:00
|
|
|
display: inline-block;
|
2021-06-05 23:03:54 +02:00
|
|
|
margin: 0;
|
|
|
|
font-weight: normal;
|
2018-03-27 10:33:31 +02:00
|
|
|
}
|
2014-08-31 17:11:42 -04:00
|
|
|
|
2015-07-08 14:52:58 +01:00
|
|
|
body.blur > :not(#help) {
|
2016-11-06 21:03:08 +01:00
|
|
|
filter: blur(8px);
|
|
|
|
-webkit-filter: blur(8px);
|
|
|
|
opacity: .7;
|
2015-07-08 14:52:58 +01:00
|
|
|
}
|
|
|
|
|
2013-09-18 22:18:38 -07:00
|
|
|
#help {
|
2016-11-06 21:03:08 +01:00
|
|
|
width: 100%;
|
|
|
|
height: 100vh;
|
|
|
|
position: fixed;
|
|
|
|
top: 0;
|
|
|
|
left: 0;
|
|
|
|
display: flex;
|
|
|
|
justify-content: center;
|
|
|
|
align-items: center;
|
2015-07-08 14:52:58 +01:00
|
|
|
}
|
|
|
|
#help > div {
|
2016-11-06 21:03:08 +01:00
|
|
|
flex: 0 0 auto;
|
|
|
|
box-shadow: 0 0 6px rgba(0,0,0,.2);
|
|
|
|
width: 550px;
|
2018-01-15 18:12:38 +01:00
|
|
|
height: auto;
|
2017-03-09 19:02:59 +01:00
|
|
|
border: 1px solid;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
|
|
|
#help dt {
|
2016-11-06 21:03:08 +01:00
|
|
|
float: left;
|
|
|
|
clear: left;
|
|
|
|
display: block;
|
2021-02-02 16:15:57 -05:00
|
|
|
margin-right: 0.5rem;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
2021-09-15 13:37:29 +02:00
|
|
|
#help span.top, #help span.bottom {
|
2020-10-19 13:44:27 +02:00
|
|
|
text-align: center;
|
|
|
|
display: block;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.125rem;
|
2021-09-15 13:37:29 +02:00
|
|
|
|
|
|
|
}
|
|
|
|
#help span.top {
|
|
|
|
text-align: center;
|
|
|
|
display: block;
|
|
|
|
margin: 10px 0;
|
|
|
|
border-bottom: 1px solid;
|
2020-10-19 13:44:27 +02:00
|
|
|
padding-bottom: 4px;
|
|
|
|
margin-bottom: 6px;
|
|
|
|
}
|
2021-09-15 13:37:29 +02:00
|
|
|
#help span.bottom {
|
|
|
|
clear: both;
|
|
|
|
border-top: 1px solid;
|
|
|
|
}
|
2017-11-07 22:44:18 +01:00
|
|
|
#help dd { margin: 5px 35px; }
|
2013-09-18 22:18:38 -07:00
|
|
|
#help .infos { padding-left: 0; }
|
2015-09-09 00:46:44 +09:00
|
|
|
#help h1, #help h2 { margin-top: 0; }
|
2015-07-08 14:52:58 +01:00
|
|
|
#help > div div {
|
2016-11-06 21:03:08 +01:00
|
|
|
width: 50%;
|
|
|
|
float: left;
|
2020-10-19 13:44:27 +02:00
|
|
|
padding: 0 20px 20px 17px;;
|
2013-09-18 22:18:38 -07:00
|
|
|
}
|
2013-09-26 12:53:06 -07:00
|
|
|
|
2021-07-18 12:25:49 +02:00
|
|
|
.item-info .stab {
|
|
|
|
display: table;
|
|
|
|
}
|
2016-12-12 17:41:39 +00:00
|
|
|
.stab {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: 3px;
|
|
|
|
margin-bottom: 5px;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 0.9rem;
|
2021-06-08 11:04:53 -07:00
|
|
|
font-weight: normal;
|
2014-06-26 11:37:39 -07:00
|
|
|
}
|
2016-12-12 17:41:39 +00:00
|
|
|
.stab p {
|
2016-11-06 21:03:08 +01:00
|
|
|
display: inline;
|
2014-06-26 11:37:39 -07:00
|
|
|
}
|
|
|
|
|
2018-12-12 22:51:04 -05:00
|
|
|
.stab .emoji {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.2rem;
|
2017-01-04 22:09:54 -08:00
|
|
|
}
|
|
|
|
|
2021-03-23 12:23:45 +01:00
|
|
|
/* Black one-pixel outline around emoji shapes */
|
|
|
|
.emoji {
|
|
|
|
text-shadow:
|
|
|
|
1px 0 0 black,
|
|
|
|
-1px 0 0 black,
|
|
|
|
0 1px 0 black,
|
|
|
|
0 -1px 0 black;
|
|
|
|
}
|
|
|
|
|
2021-04-13 17:23:27 +02:00
|
|
|
.module-item .stab,
|
|
|
|
.import-item .stab {
|
2019-01-14 10:02:27 -05:00
|
|
|
border-radius: 3px;
|
|
|
|
display: inline-block;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 0.8rem;
|
2019-01-14 10:02:27 -05:00
|
|
|
line-height: 1.2;
|
|
|
|
margin-bottom: 0;
|
2021-06-23 20:02:00 +02:00
|
|
|
margin-left: .3em;
|
2019-01-14 10:02:27 -05:00
|
|
|
padding: 2px;
|
|
|
|
vertical-align: text-bottom;
|
2013-09-26 12:53:06 -07:00
|
|
|
}
|
2014-03-18 01:44:55 -06:00
|
|
|
|
2021-04-13 17:23:27 +02:00
|
|
|
.module-item.unstable,
|
|
|
|
.import-item.unstable {
|
2016-11-06 21:03:08 +01:00
|
|
|
opacity: 0.65;
|
2015-04-13 11:55:00 -07:00
|
|
|
}
|
2014-02-16 21:56:14 -08:00
|
|
|
|
2016-05-06 18:47:12 +02:00
|
|
|
.since {
|
2016-11-06 21:03:08 +01:00
|
|
|
font-weight: normal;
|
|
|
|
font-size: initial;
|
2016-02-09 21:15:29 -05:00
|
|
|
}
|
|
|
|
|
2021-12-03 17:09:04 -08:00
|
|
|
.rightside {
|
2018-12-26 21:23:05 -08:00
|
|
|
padding-left: 12px;
|
|
|
|
padding-right: 2px;
|
|
|
|
position: initial;
|
|
|
|
}
|
|
|
|
|
2020-11-18 13:38:17 +00:00
|
|
|
.impl-items .srclink, .impl .srclink, .methods .srclink {
|
2018-12-26 21:23:05 -08:00
|
|
|
/* Override header settings otherwise it's too bold */
|
|
|
|
font-weight: normal;
|
2021-12-29 14:55:49 +01:00
|
|
|
font-size: 1rem;
|
|
|
|
}
|
|
|
|
.impl .srclink {
|
|
|
|
font-size: 1.0625rem;
|
2018-12-26 21:23:05 -08:00
|
|
|
}
|
|
|
|
|
2021-06-08 11:04:53 -07:00
|
|
|
.rightside {
|
|
|
|
float: right;
|
2018-12-26 21:23:05 -08:00
|
|
|
}
|
|
|
|
|
2021-06-01 21:43:09 -07:00
|
|
|
.has-srclink {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2018-12-26 21:23:05 -08:00
|
|
|
margin-bottom: 12px;
|
|
|
|
/* Push the src link out to the right edge consistently */
|
|
|
|
justify-content: space-between;
|
|
|
|
}
|
|
|
|
|
2016-02-09 21:15:29 -05:00
|
|
|
.variants_table {
|
2016-11-06 21:03:08 +01:00
|
|
|
width: 100%;
|
2016-02-09 21:15:29 -05:00
|
|
|
}
|
|
|
|
|
|
|
|
.variants_table tbody tr td:first-child {
|
2016-11-06 21:03:08 +01:00
|
|
|
width: 1%; /* make the variant name as small as possible */
|
2016-02-09 21:15:29 -05:00
|
|
|
}
|
|
|
|
|
2015-03-29 15:14:02 -04:00
|
|
|
td.summary-column {
|
2016-11-06 21:03:08 +01:00
|
|
|
width: 100%;
|
2015-03-29 15:14:02 -04:00
|
|
|
}
|
|
|
|
|
2014-07-04 00:51:46 -07:00
|
|
|
.summary {
|
2016-11-06 21:03:08 +01:00
|
|
|
padding-right: 0px;
|
2014-07-04 00:51:46 -07:00
|
|
|
}
|
|
|
|
|
2016-10-12 05:23:37 +02:00
|
|
|
pre.rust .question-mark {
|
2016-11-06 21:03:08 +01:00
|
|
|
font-weight: bold;
|
2016-10-12 05:23:37 +02:00
|
|
|
}
|
2014-03-04 11:24:20 -08:00
|
|
|
|
2015-10-14 15:05:21 -04:00
|
|
|
a.test-arrow {
|
2016-11-06 21:03:08 +01:00
|
|
|
display: inline-block;
|
2021-12-17 22:38:18 -08:00
|
|
|
visibility: hidden;
|
2016-11-06 21:03:08 +01:00
|
|
|
position: absolute;
|
|
|
|
padding: 5px 10px 5px 10px;
|
|
|
|
border-radius: 5px;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.3rem;
|
2016-11-06 21:03:08 +01:00
|
|
|
top: 5px;
|
|
|
|
right: 5px;
|
2020-01-26 17:24:40 +01:00
|
|
|
z-index: 1;
|
2014-06-06 09:12:18 -07:00
|
|
|
}
|
2021-12-17 22:38:18 -08:00
|
|
|
.example-wrap:hover .test-arrow {
|
|
|
|
visibility: visible;
|
|
|
|
}
|
2016-09-08 01:16:06 +02:00
|
|
|
a.test-arrow:hover{
|
2016-11-06 21:03:08 +01:00
|
|
|
text-decoration: none;
|
2016-09-08 01:16:06 +02:00
|
|
|
}
|
2017-09-17 22:11:37 +02:00
|
|
|
.section-header:hover a:before {
|
|
|
|
position: absolute;
|
|
|
|
left: -25px;
|
2018-08-25 14:15:49 -07:00
|
|
|
padding-right: 10px; /* avoid gap that causes hover to disappear */
|
2016-11-06 21:03:08 +01:00
|
|
|
content: '\2002\00a7\2002';
|
2014-03-08 01:24:54 +11:00
|
|
|
}
|
2014-03-19 16:33:03 -06:00
|
|
|
|
2015-02-20 13:54:11 +02:00
|
|
|
.section-header:hover a {
|
2016-11-06 21:03:08 +01:00
|
|
|
text-decoration: none;
|
2015-02-20 13:54:11 +02:00
|
|
|
}
|
|
|
|
|
2021-04-17 18:08:50 -07:00
|
|
|
.code-attribute {
|
|
|
|
font-weight: 300;
|
|
|
|
}
|
|
|
|
|
2017-07-09 00:40:29 +02:00
|
|
|
.item-spacer {
|
|
|
|
width: 100%;
|
|
|
|
height: 12px;
|
|
|
|
}
|
|
|
|
|
2019-05-03 12:55:31 -04:00
|
|
|
.out-of-band > span.since {
|
2016-11-06 21:03:08 +01:00
|
|
|
position: initial;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.25rem;
|
2016-11-06 21:03:08 +01:00
|
|
|
margin-right: 5px;
|
2016-05-10 21:01:10 +02:00
|
|
|
}
|
|
|
|
|
2021-10-19 22:48:53 -07:00
|
|
|
h3.variant {
|
|
|
|
font-weight: 600;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.1rem;
|
2021-10-19 22:48:53 -07:00
|
|
|
margin-bottom: 10px;
|
|
|
|
border-bottom: none;
|
2018-10-19 01:34:46 +02:00
|
|
|
}
|
|
|
|
|
2021-10-19 22:48:53 -07:00
|
|
|
.sub-variant h4 {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2021-10-19 22:48:53 -07:00
|
|
|
font-weight: 400;
|
|
|
|
border-bottom: none;
|
|
|
|
margin-top: 0;
|
|
|
|
margin-bottom: 0;
|
2018-10-19 01:34:46 +02:00
|
|
|
}
|
|
|
|
|
2021-10-19 22:48:53 -07:00
|
|
|
.sub-variant {
|
|
|
|
margin-left: 24px;
|
|
|
|
margin-bottom: 40px;
|
2018-10-19 01:34:46 +02:00
|
|
|
}
|
|
|
|
|
2021-10-19 22:48:53 -07:00
|
|
|
.sub-variant > .sub-variant-field {
|
|
|
|
margin-left: 24px;
|
2016-11-11 16:41:00 -06:00
|
|
|
}
|
|
|
|
|
2017-08-30 23:16:25 +02:00
|
|
|
.toggle-label {
|
|
|
|
display: inline-block;
|
|
|
|
margin-left: 4px;
|
|
|
|
margin-top: 3px;
|
|
|
|
}
|
|
|
|
|
2021-11-25 15:33:38 +01:00
|
|
|
.top-doc .docblock > .section-header:first-child {
|
2017-10-22 16:08:31 +02:00
|
|
|
margin-left: 15px;
|
|
|
|
}
|
2021-11-25 15:33:38 +01:00
|
|
|
.top-doc .docblock > .section-header:first-child:hover > a:before {
|
2017-10-22 16:08:31 +02:00
|
|
|
left: -10px;
|
|
|
|
}
|
|
|
|
|
2021-11-25 15:33:38 +01:00
|
|
|
.docblock > .section-header:first-child {
|
|
|
|
margin-top: 0;
|
|
|
|
}
|
|
|
|
|
2021-07-25 21:41:57 +00:00
|
|
|
:target > code, :target > .code-header {
|
2017-03-09 19:02:59 +01:00
|
|
|
opacity: 1;
|
2016-05-16 22:36:13 +02:00
|
|
|
}
|
|
|
|
|
2021-06-16 22:48:23 -07:00
|
|
|
:target {
|
|
|
|
padding-right: 3px;
|
|
|
|
}
|
|
|
|
|
2017-09-09 15:33:57 +02:00
|
|
|
.information {
|
|
|
|
position: absolute;
|
2020-03-14 18:17:08 +01:00
|
|
|
left: -25px;
|
2017-09-09 15:33:57 +02:00
|
|
|
margin-top: 7px;
|
2017-09-18 12:51:48 +02:00
|
|
|
z-index: 1;
|
2017-09-09 15:33:57 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
.tooltip {
|
|
|
|
position: relative;
|
|
|
|
display: inline-block;
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
2020-12-05 17:31:31 +01:00
|
|
|
.tooltip::after {
|
2017-09-09 15:33:57 +02:00
|
|
|
display: none;
|
|
|
|
text-align: center;
|
2020-03-14 18:17:08 +01:00
|
|
|
padding: 5px 3px 3px 3px;
|
2017-09-09 15:33:57 +02:00
|
|
|
border-radius: 6px;
|
|
|
|
margin-left: 5px;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2017-09-09 15:33:57 +02:00
|
|
|
}
|
|
|
|
|
2020-12-05 17:31:31 +01:00
|
|
|
.tooltip.ignore::after {
|
|
|
|
content: "This example is not tested";
|
|
|
|
}
|
|
|
|
.tooltip.compile_fail::after {
|
|
|
|
content: "This example deliberately fails to compile";
|
|
|
|
}
|
|
|
|
.tooltip.should_panic::after {
|
|
|
|
content: "This example panics";
|
|
|
|
}
|
|
|
|
.tooltip.edition::after {
|
2020-12-23 20:27:12 +01:00
|
|
|
content: "This code runs with edition " attr(data-edition);
|
2020-12-05 17:31:31 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
.tooltip::before {
|
2017-09-09 15:33:57 +02:00
|
|
|
content: " ";
|
|
|
|
position: absolute;
|
|
|
|
top: 50%;
|
2020-03-14 18:17:08 +01:00
|
|
|
left: 16px;
|
2017-09-09 15:33:57 +02:00
|
|
|
margin-top: -5px;
|
|
|
|
border-width: 5px;
|
|
|
|
border-style: solid;
|
2020-12-05 17:31:31 +01:00
|
|
|
display: none;
|
2017-09-09 15:33:57 +02:00
|
|
|
}
|
2017-09-18 12:51:48 +02:00
|
|
|
|
2020-12-05 17:31:31 +01:00
|
|
|
.tooltip:hover::before, .tooltip:hover::after {
|
2020-10-07 11:31:15 +02:00
|
|
|
display: inline;
|
|
|
|
}
|
|
|
|
|
2020-06-18 08:48:37 -04:00
|
|
|
.tooltip.compile_fail, .tooltip.should_panic, .tooltip.ignore {
|
2020-03-14 18:17:08 +01:00
|
|
|
font-weight: bold;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.25rem;
|
2020-03-14 18:17:08 +01:00
|
|
|
}
|
|
|
|
|
2020-08-09 12:09:05 -07:00
|
|
|
.notable-traits-tooltip {
|
2020-07-06 17:18:04 -07:00
|
|
|
display: inline-block;
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
2020-08-09 12:09:05 -07:00
|
|
|
.notable-traits:hover .notable-traits-tooltiptext,
|
|
|
|
.notable-traits .notable-traits-tooltiptext.force-tooltip {
|
2020-07-06 17:18:04 -07:00
|
|
|
display: inline-block;
|
|
|
|
}
|
|
|
|
|
2020-08-09 12:09:05 -07:00
|
|
|
.notable-traits .notable-traits-tooltiptext {
|
2020-07-06 17:18:04 -07:00
|
|
|
display: none;
|
|
|
|
padding: 5px 3px 3px 3px;
|
|
|
|
border-radius: 6px;
|
|
|
|
margin-left: 5px;
|
|
|
|
z-index: 10;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2020-07-06 17:18:04 -07:00
|
|
|
cursor: default;
|
|
|
|
position: absolute;
|
2020-07-15 09:29:34 -07:00
|
|
|
border: 1px solid;
|
2020-07-06 17:18:04 -07:00
|
|
|
}
|
|
|
|
|
2020-08-09 12:09:05 -07:00
|
|
|
.notable-traits-tooltip::after {
|
2020-07-06 17:18:04 -07:00
|
|
|
/* The margin on the tooltip does not capture hover events,
|
|
|
|
this extends the area of hover enough so that mouse hover is not
|
|
|
|
lost when moving the mouse to the tooltip */
|
2020-07-15 17:20:46 +02:00
|
|
|
content: "\00a0\00a0\00a0";
|
2020-07-06 17:18:04 -07:00
|
|
|
}
|
|
|
|
|
2020-08-09 12:09:05 -07:00
|
|
|
.notable-traits .notable, .notable-traits .docblock {
|
2020-07-06 17:18:04 -07:00
|
|
|
margin: 0;
|
|
|
|
}
|
|
|
|
|
2021-06-02 21:16:33 +02:00
|
|
|
.notable-traits .notable {
|
|
|
|
margin: 0;
|
|
|
|
margin-bottom: 13px;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.1875rem;
|
2021-06-02 21:16:33 +02:00
|
|
|
font-weight: 600;
|
|
|
|
}
|
|
|
|
|
2020-08-09 12:09:05 -07:00
|
|
|
.notable-traits .docblock code.content{
|
2020-07-15 17:20:46 +02:00
|
|
|
margin: 0;
|
|
|
|
padding: 0;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.25rem;
|
2017-11-29 19:23:41 +01:00
|
|
|
}
|
|
|
|
|
2020-07-15 17:20:46 +02:00
|
|
|
/* Example code has the "Run" button that needs to be positioned relative to the pre */
|
2020-07-16 09:01:30 -07:00
|
|
|
pre.rust.rust-example-rendered {
|
2017-09-18 12:51:48 +02:00
|
|
|
position: relative;
|
2020-07-16 09:01:30 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
pre.rust {
|
2020-03-28 11:49:12 +01:00
|
|
|
tab-size: 4;
|
|
|
|
-moz-tab-size: 4;
|
2017-09-18 12:51:48 +02:00
|
|
|
}
|
2017-10-04 00:06:07 +02:00
|
|
|
|
|
|
|
.search-failed {
|
|
|
|
text-align: center;
|
|
|
|
margin-top: 20px;
|
2021-05-09 12:56:21 -07:00
|
|
|
display: none;
|
|
|
|
}
|
|
|
|
|
|
|
|
.search-failed.active {
|
|
|
|
display: block;
|
2017-10-04 00:06:07 +02:00
|
|
|
}
|
|
|
|
|
2018-11-01 02:20:49 +01:00
|
|
|
.search-failed > ul {
|
|
|
|
text-align: left;
|
|
|
|
max-width: 570px;
|
|
|
|
margin-left: auto;
|
|
|
|
margin-right: auto;
|
|
|
|
}
|
|
|
|
|
2017-10-04 00:06:07 +02:00
|
|
|
#titles {
|
|
|
|
height: 35px;
|
|
|
|
}
|
|
|
|
|
2020-12-10 11:38:12 +01:00
|
|
|
#titles > button {
|
2017-10-04 00:06:07 +02:00
|
|
|
float: left;
|
|
|
|
width: 33.3%;
|
|
|
|
text-align: center;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.125rem;
|
2017-10-04 00:06:07 +02:00
|
|
|
cursor: pointer;
|
2020-12-10 11:38:12 +01:00
|
|
|
border: 0;
|
2018-10-16 19:07:41 +02:00
|
|
|
border-top: 2px solid;
|
2017-10-04 00:06:07 +02:00
|
|
|
}
|
|
|
|
|
2020-12-10 11:38:12 +01:00
|
|
|
#titles > button:not(:last-child) {
|
2018-10-16 19:07:41 +02:00
|
|
|
margin-right: 1px;
|
|
|
|
width: calc(33.3% - 1px);
|
2017-10-04 00:06:07 +02:00
|
|
|
}
|
2017-11-02 01:01:51 +01:00
|
|
|
|
2020-12-10 11:38:12 +01:00
|
|
|
#titles > button > div.count {
|
2017-11-02 01:01:51 +01:00
|
|
|
display: inline-block;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2017-11-02 01:01:51 +01:00
|
|
|
}
|
2017-11-15 20:04:02 +01:00
|
|
|
|
2020-08-09 12:09:05 -07:00
|
|
|
.notable-traits {
|
2020-07-06 12:53:44 -07:00
|
|
|
cursor: pointer;
|
|
|
|
z-index: 2;
|
2020-07-06 14:13:47 -07:00
|
|
|
margin-left: 5px;
|
2020-07-06 12:53:44 -07:00
|
|
|
}
|
|
|
|
|
2018-10-06 18:51:56 +02:00
|
|
|
#all-types {
|
|
|
|
text-align: center;
|
|
|
|
border: 1px solid;
|
|
|
|
margin: 0 10px;
|
|
|
|
margin-bottom: 10px;
|
|
|
|
display: block;
|
|
|
|
border-radius: 7px;
|
|
|
|
}
|
|
|
|
#all-types > p {
|
|
|
|
margin: 5px 0;
|
|
|
|
}
|
|
|
|
|
2019-04-29 23:24:09 +02:00
|
|
|
#sidebar-toggle {
|
2021-10-24 21:59:53 +02:00
|
|
|
position: sticky;
|
|
|
|
top: 0;
|
|
|
|
left: 0;
|
2019-04-29 23:24:09 +02:00
|
|
|
cursor: pointer;
|
|
|
|
font-weight: bold;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.2rem;
|
2021-10-24 21:59:53 +02:00
|
|
|
border-bottom: 1px solid;
|
|
|
|
display: flex;
|
|
|
|
height: 40px;
|
|
|
|
justify-content: center;
|
|
|
|
align-items: center;
|
|
|
|
z-index: 10;
|
2019-04-29 23:24:09 +02:00
|
|
|
}
|
|
|
|
#source-sidebar {
|
2021-12-14 11:48:30 +01:00
|
|
|
width: 100%;
|
2019-04-29 23:24:09 +02:00
|
|
|
z-index: 1;
|
|
|
|
overflow: auto;
|
|
|
|
}
|
|
|
|
#source-sidebar > .title {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.5rem;
|
2019-04-29 23:24:09 +02:00
|
|
|
text-align: center;
|
|
|
|
border-bottom: 1px solid;
|
|
|
|
margin-bottom: 6px;
|
|
|
|
}
|
|
|
|
|
2019-04-29 23:43:39 +02:00
|
|
|
.theme-picker {
|
|
|
|
position: absolute;
|
2021-10-10 00:52:14 +02:00
|
|
|
left: -34px;
|
|
|
|
top: 9px;
|
2019-04-29 23:43:39 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
.theme-picker button {
|
|
|
|
outline: none;
|
|
|
|
}
|
|
|
|
|
2021-05-09 11:21:38 -07:00
|
|
|
#settings-menu, #help-button {
|
2019-04-29 23:43:39 +02:00
|
|
|
position: absolute;
|
|
|
|
top: 10px;
|
2020-08-10 16:42:11 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
#settings-menu {
|
|
|
|
right: 0;
|
2019-04-29 23:43:39 +02:00
|
|
|
outline: none;
|
|
|
|
}
|
|
|
|
|
2021-05-09 11:21:38 -07:00
|
|
|
#theme-picker, #settings-menu, #help-button, #copy-path {
|
2021-03-31 22:13:47 +02:00
|
|
|
padding: 4px;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
/* Rare exception to specifying font sizes in rem. Since these are acting
|
|
|
|
as icons, it's okay to specify their sizes in pixels. */
|
|
|
|
font-size: 16px;
|
2021-03-31 22:13:47 +02:00
|
|
|
width: 27px;
|
|
|
|
height: 29px;
|
|
|
|
border: 1px solid;
|
|
|
|
border-radius: 3px;
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
2021-05-09 11:21:38 -07:00
|
|
|
#help-button {
|
2020-08-10 16:42:11 +02:00
|
|
|
right: 30px;
|
2021-03-15 19:20:15 +02:00
|
|
|
font-family: "Fira Sans", Arial, sans-serif;
|
2020-08-10 16:42:11 +02:00
|
|
|
text-align: center;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
/* Rare exception to specifying font sizes in rem. Since this is acting
|
|
|
|
as an icon, it's okay to specify their sizes in pixels. */
|
|
|
|
font-size: 16px;
|
2021-03-31 22:13:47 +02:00
|
|
|
padding-top: 2px;
|
2020-08-10 16:42:11 +02:00
|
|
|
}
|
|
|
|
|
2021-03-31 22:13:47 +02:00
|
|
|
#copy-path {
|
2021-05-17 13:26:58 +02:00
|
|
|
background: initial;
|
2021-03-31 22:13:47 +02:00
|
|
|
margin-left: 10px;
|
2021-05-09 20:41:24 +02:00
|
|
|
padding: 0;
|
|
|
|
padding-left: 2px;
|
2021-05-17 13:26:58 +02:00
|
|
|
border: 0;
|
2019-04-29 23:43:39 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
#theme-choices {
|
|
|
|
display: none;
|
|
|
|
position: absolute;
|
|
|
|
left: 0;
|
|
|
|
top: 28px;
|
|
|
|
border: 1px solid;
|
|
|
|
border-radius: 3px;
|
|
|
|
z-index: 1;
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
|
|
|
#theme-choices > button {
|
|
|
|
border: none;
|
|
|
|
width: 100%;
|
2020-08-24 22:32:59 +08:00
|
|
|
padding: 4px 8px;
|
2019-04-29 23:43:39 +02:00
|
|
|
text-align: center;
|
|
|
|
background: rgba(0,0,0,0);
|
2022-01-11 17:36:52 -08:00
|
|
|
overflow-wrap: normal;
|
2019-04-29 23:43:39 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
#theme-choices > button:not(:first-child) {
|
|
|
|
border-top: 1px solid;
|
|
|
|
}
|
|
|
|
|
2021-05-14 19:43:08 +02:00
|
|
|
kbd {
|
|
|
|
display: inline-block;
|
|
|
|
padding: 3px 5px;
|
|
|
|
font: 15px monospace;
|
|
|
|
line-height: 10px;
|
|
|
|
vertical-align: middle;
|
|
|
|
border: solid 1px;
|
|
|
|
border-radius: 3px;
|
|
|
|
box-shadow: inset 0 -1px 0;
|
|
|
|
cursor: default;
|
|
|
|
}
|
|
|
|
|
|
|
|
.hidden-by-impl-hider,
|
|
|
|
.hidden-by-usual-hider {
|
|
|
|
/* important because of conflicting rule for small screens */
|
|
|
|
display: none !important;
|
|
|
|
}
|
|
|
|
|
|
|
|
#implementations-list > h3 > span.in-band {
|
|
|
|
width: 100%;
|
|
|
|
}
|
|
|
|
|
|
|
|
.table-display {
|
|
|
|
width: 100%;
|
|
|
|
border: 0;
|
|
|
|
border-collapse: collapse;
|
|
|
|
border-spacing: 0;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2021-05-14 19:43:08 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
.table-display tr td:first-child {
|
|
|
|
padding-right: 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
.table-display tr td:last-child {
|
|
|
|
float: right;
|
|
|
|
}
|
|
|
|
.table-display .out-of-band {
|
|
|
|
position: relative;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.1875rem;
|
2021-05-14 19:43:08 +02:00
|
|
|
display: block;
|
|
|
|
}
|
|
|
|
#implementors-list > .impl-items .table-display .out-of-band {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.0625rem;
|
2021-05-14 19:43:08 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
.table-display td:hover .anchor {
|
|
|
|
display: block;
|
|
|
|
top: 2px;
|
|
|
|
left: -5px;
|
|
|
|
}
|
|
|
|
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content > ul {
|
2021-05-14 19:43:08 +02:00
|
|
|
padding-left: 10px;
|
|
|
|
}
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content > ul > li {
|
2021-05-14 19:43:08 +02:00
|
|
|
list-style: none;
|
|
|
|
}
|
|
|
|
|
|
|
|
.non-exhaustive {
|
|
|
|
margin-bottom: 1em;
|
|
|
|
}
|
|
|
|
|
|
|
|
div.children {
|
|
|
|
padding-left: 27px;
|
|
|
|
display: none;
|
|
|
|
}
|
|
|
|
div.name {
|
|
|
|
cursor: pointer;
|
|
|
|
position: relative;
|
|
|
|
margin-left: 16px;
|
|
|
|
}
|
|
|
|
div.files > a {
|
|
|
|
display: block;
|
|
|
|
padding: 0 3px;
|
|
|
|
}
|
|
|
|
div.files > a:hover, div.name:hover {
|
|
|
|
background-color: #a14b4b;
|
|
|
|
}
|
|
|
|
div.name.expand + .children {
|
|
|
|
display: block;
|
|
|
|
}
|
|
|
|
div.name::before {
|
|
|
|
content: "\25B6";
|
|
|
|
padding-left: 4px;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 0.7rem;
|
2021-05-14 19:43:08 +02:00
|
|
|
position: absolute;
|
|
|
|
left: -16px;
|
|
|
|
top: 4px;
|
|
|
|
}
|
|
|
|
div.name.expand::before {
|
|
|
|
transform: rotate(90deg);
|
|
|
|
left: -15px;
|
|
|
|
top: 2px;
|
|
|
|
}
|
|
|
|
|
|
|
|
/* The hideme class is used on summary tags that contain a span with
|
|
|
|
placeholder text shown only when the toggle is closed. For instance,
|
|
|
|
"Expand description" or "Show methods". */
|
|
|
|
details.rustdoc-toggle > summary.hideme {
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
2021-11-20 23:46:23 -08:00
|
|
|
details.rustdoc-toggle > summary {
|
2021-05-14 19:43:08 +02:00
|
|
|
list-style: none;
|
|
|
|
}
|
|
|
|
details.rustdoc-toggle > summary::-webkit-details-marker,
|
2021-11-20 23:46:23 -08:00
|
|
|
details.rustdoc-toggle > summary::marker {
|
2021-05-14 19:43:08 +02:00
|
|
|
display: none;
|
|
|
|
}
|
|
|
|
|
|
|
|
details.rustdoc-toggle > summary.hideme > span {
|
|
|
|
margin-left: 9px;
|
|
|
|
}
|
|
|
|
|
|
|
|
details.rustdoc-toggle > summary::before {
|
2021-07-17 11:28:26 -07:00
|
|
|
content: "";
|
2021-05-14 19:43:08 +02:00
|
|
|
cursor: pointer;
|
2021-07-16 17:24:35 -07:00
|
|
|
width: 17px;
|
|
|
|
height: max(17px, 1.1em);
|
2021-07-31 16:23:51 +02:00
|
|
|
background-repeat: no-repeat;
|
|
|
|
background-position: top left;
|
2021-07-16 17:24:35 -07:00
|
|
|
display: inline-block;
|
|
|
|
vertical-align: middle;
|
|
|
|
opacity: .5;
|
2021-07-17 10:55:33 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
/* Screen readers see the text version at the end the line.
|
|
|
|
Visual readers see the icon at the start of the line, but small and transparent. */
|
|
|
|
details.rustdoc-toggle > summary::after {
|
|
|
|
content: "Expand";
|
2021-07-16 17:24:35 -07:00
|
|
|
overflow: hidden;
|
2021-07-17 10:55:33 -07:00
|
|
|
width: 0;
|
|
|
|
height: 0;
|
|
|
|
position: absolute;
|
2021-07-16 17:24:35 -07:00
|
|
|
}
|
|
|
|
|
2021-07-17 10:55:33 -07:00
|
|
|
details.rustdoc-toggle > summary.hideme::after {
|
2021-07-16 17:24:35 -07:00
|
|
|
/* "hideme" toggles already have a description when they're contracted */
|
2021-07-17 10:55:33 -07:00
|
|
|
content: "";
|
2021-07-16 17:24:35 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
details.rustdoc-toggle > summary:focus::before,
|
|
|
|
details.rustdoc-toggle > summary:hover::before {
|
|
|
|
opacity: 1;
|
2021-05-14 19:43:08 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
details.rustdoc-toggle.top-doc > summary,
|
|
|
|
details.rustdoc-toggle.top-doc > summary::before,
|
|
|
|
details.rustdoc-toggle.non-exhaustive > summary,
|
|
|
|
details.rustdoc-toggle.non-exhaustive > summary::before {
|
|
|
|
font-family: 'Fira Sans';
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1rem;
|
2021-05-14 19:43:08 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
details.non-exhaustive {
|
|
|
|
margin-bottom: 8px;
|
|
|
|
}
|
|
|
|
|
|
|
|
details.rustdoc-toggle > summary.hideme::before {
|
|
|
|
position: relative;
|
|
|
|
}
|
|
|
|
|
|
|
|
details.rustdoc-toggle > summary:not(.hideme)::before {
|
|
|
|
position: absolute;
|
2021-10-21 18:46:47 -07:00
|
|
|
left: -24px;
|
2021-05-31 23:18:53 +08:00
|
|
|
top: 3px;
|
2021-05-14 19:43:08 +02:00
|
|
|
}
|
|
|
|
|
2021-11-20 23:46:23 -08:00
|
|
|
.impl-items > details.rustdoc-toggle > summary:not(.hideme)::before {
|
2021-05-14 19:43:08 +02:00
|
|
|
position: absolute;
|
2021-10-21 18:46:47 -07:00
|
|
|
left: -24px;
|
2021-05-14 19:43:08 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
/* When a "hideme" summary is open and the "Expand description" or "Show
|
|
|
|
methods" text is hidden, we want the [-] toggle that remains to not
|
|
|
|
affect the layout of the items to its right. To do that, we use
|
|
|
|
absolute positioning. Note that we also set position: relative
|
|
|
|
on the parent <details> to make this work properly. */
|
|
|
|
details.rustdoc-toggle[open] > summary.hideme {
|
|
|
|
position: absolute;
|
|
|
|
}
|
|
|
|
|
2021-11-20 23:46:23 -08:00
|
|
|
details.rustdoc-toggle {
|
2021-05-14 19:43:08 +02:00
|
|
|
position: relative;
|
|
|
|
}
|
|
|
|
|
|
|
|
details.rustdoc-toggle[open] > summary.hideme > span {
|
|
|
|
display: none;
|
|
|
|
}
|
|
|
|
|
2021-11-23 21:23:54 -08:00
|
|
|
details.undocumented[open] > summary::before,
|
|
|
|
details.rustdoc-toggle[open] > summary::before,
|
|
|
|
details.rustdoc-toggle[open] > summary.hideme::before {
|
|
|
|
background-image: /* AUTOREPLACE: */url("toggle-minus.svg");
|
|
|
|
}
|
|
|
|
|
|
|
|
details.undocumented > summary::before, details.rustdoc-toggle > summary::before {
|
|
|
|
background-image: /* AUTOREPLACE: */url("toggle-plus.svg");
|
|
|
|
}
|
|
|
|
|
2021-07-16 17:24:35 -07:00
|
|
|
details.rustdoc-toggle[open] > summary::before,
|
|
|
|
details.rustdoc-toggle[open] > summary.hideme::before {
|
|
|
|
width: 17px;
|
|
|
|
height: max(17px, 1.1em);
|
2021-07-31 16:23:51 +02:00
|
|
|
background-repeat: no-repeat;
|
|
|
|
background-position: top left;
|
2021-07-16 17:24:35 -07:00
|
|
|
display: inline-block;
|
2021-07-17 11:28:26 -07:00
|
|
|
content: "";
|
2021-07-17 10:55:33 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
details.rustdoc-toggle[open] > summary::after,
|
|
|
|
details.rustdoc-toggle[open] > summary.hideme::after {
|
2021-07-16 17:24:35 -07:00
|
|
|
content: "Collapse";
|
2021-05-14 19:43:08 +02:00
|
|
|
}
|
|
|
|
|
2014-08-02 20:58:41 -04:00
|
|
|
/* Media Queries */
|
|
|
|
|
2020-07-22 16:28:47 +02:00
|
|
|
@media (min-width: 701px) {
|
|
|
|
/* In case there is no documentation before a code block, we need to add some margin at the top
|
|
|
|
to prevent an overlay between the "collapse toggle" and the information tooltip.
|
2021-03-09 21:14:43 +01:00
|
|
|
However, it's not needed with smaller screen width because the doc/code block is always put
|
2020-07-22 16:28:47 +02:00
|
|
|
"one line" below. */
|
2021-03-22 22:17:21 +01:00
|
|
|
.docblock > .information:first-child > .tooltip {
|
2020-07-22 16:28:47 +02:00
|
|
|
margin-top: 16px;
|
|
|
|
}
|
2021-11-29 15:55:05 +01:00
|
|
|
|
|
|
|
/* When we expand the sidebar on the source code page, we hide the logo on the left of the
|
|
|
|
search bar to have more space. */
|
2021-12-02 14:21:32 +01:00
|
|
|
.sidebar.expanded + main .width-limiter .sub-logo-container.rust-logo {
|
2021-11-29 15:55:05 +01:00
|
|
|
display: none;
|
|
|
|
}
|
|
|
|
|
|
|
|
/* It doesn't render well on mobile because of the layout, so better only have the transition
|
|
|
|
on desktop. */
|
|
|
|
.rustdoc.source .sidebar {
|
|
|
|
transition: width .5s;
|
|
|
|
}
|
2021-12-14 11:48:30 +01:00
|
|
|
|
|
|
|
.source .sidebar.expanded {
|
|
|
|
width: 300px;
|
|
|
|
}
|
2020-07-22 16:28:47 +02:00
|
|
|
}
|
|
|
|
|
2014-08-02 20:58:41 -04:00
|
|
|
@media (max-width: 700px) {
|
2016-11-06 21:03:08 +01:00
|
|
|
body {
|
|
|
|
padding-top: 0px;
|
|
|
|
}
|
|
|
|
|
2021-09-30 04:23:02 +02:00
|
|
|
main {
|
|
|
|
padding-left: 15px;
|
|
|
|
padding-top: 0px;
|
|
|
|
}
|
|
|
|
|
2022-01-05 22:20:26 -05:00
|
|
|
/* Space is at a premium on mobile, so remove the theme-picker icon. */
|
|
|
|
#theme-picker {
|
|
|
|
display: none;
|
|
|
|
width: 0;
|
|
|
|
}
|
|
|
|
|
2021-09-30 04:23:02 +02:00
|
|
|
.rustdoc {
|
|
|
|
flex-direction: column;
|
|
|
|
}
|
|
|
|
|
2021-10-10 19:08:08 +02:00
|
|
|
.rustdoc:not(.source) > .sidebar {
|
2021-09-30 04:23:02 +02:00
|
|
|
width: 100%;
|
2017-10-12 20:00:34 +02:00
|
|
|
height: 45px;
|
2016-11-06 21:03:08 +01:00
|
|
|
min-height: 40px;
|
2021-09-30 04:23:02 +02:00
|
|
|
max-height: 45px;
|
2017-10-12 20:00:34 +02:00
|
|
|
margin: 0;
|
|
|
|
padding: 0 15px;
|
2016-11-06 21:03:08 +01:00
|
|
|
position: static;
|
2018-12-18 13:55:30 -08:00
|
|
|
z-index: 11;
|
2021-11-29 15:55:05 +01:00
|
|
|
overflow-y: hidden;
|
2016-11-06 21:03:08 +01:00
|
|
|
}
|
|
|
|
|
2021-10-10 19:08:08 +02:00
|
|
|
.rustdoc.source > .sidebar {
|
|
|
|
position: fixed;
|
|
|
|
top: 0;
|
|
|
|
left: 0;
|
|
|
|
margin: 0;
|
|
|
|
z-index: 11;
|
2021-10-24 21:59:53 +02:00
|
|
|
width: 0;
|
2021-10-10 19:08:08 +02:00
|
|
|
}
|
|
|
|
|
2021-10-24 20:03:13 +02:00
|
|
|
.sidebar.mobile {
|
|
|
|
position: sticky !important;
|
|
|
|
top: 0;
|
|
|
|
left: 0;
|
|
|
|
width: 100%;
|
|
|
|
margin-left: 0;
|
|
|
|
background-color: rgba(0,0,0,0);
|
|
|
|
}
|
|
|
|
|
2017-12-06 00:42:33 +01:00
|
|
|
.sidebar > .location {
|
2016-11-06 21:03:08 +01:00
|
|
|
float: right;
|
|
|
|
margin: 0px;
|
2017-10-12 20:00:34 +02:00
|
|
|
margin-top: 2px;
|
2016-11-06 21:03:08 +01:00
|
|
|
padding: 3px 10px 1px 10px;
|
|
|
|
min-height: 39px;
|
|
|
|
background: inherit;
|
|
|
|
text-align: left;
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.5rem;
|
2016-11-06 21:03:08 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
.sidebar .location:empty {
|
|
|
|
padding: 0;
|
|
|
|
}
|
|
|
|
|
2021-10-10 19:08:08 +02:00
|
|
|
.rustdoc:not(.source) .sidebar .logo-container {
|
2016-11-06 21:03:08 +01:00
|
|
|
width: 35px;
|
2021-10-24 20:05:50 +02:00
|
|
|
height: 35px;
|
|
|
|
margin-top: 5px;
|
|
|
|
margin-bottom: 5px;
|
|
|
|
float: left;
|
|
|
|
margin-left: 50px;
|
2016-11-06 21:03:08 +01:00
|
|
|
}
|
|
|
|
|
2019-04-29 11:45:06 +02:00
|
|
|
.sidebar .logo-container > img {
|
|
|
|
max-width: 35px;
|
|
|
|
max-height: 35px;
|
|
|
|
}
|
|
|
|
|
2017-12-06 00:42:33 +01:00
|
|
|
.sidebar-menu {
|
2017-12-11 22:30:04 +01:00
|
|
|
position: fixed;
|
|
|
|
z-index: 10;
|
2017-12-06 00:42:33 +01:00
|
|
|
font-size: 2rem;
|
|
|
|
cursor: pointer;
|
2017-12-11 22:30:04 +01:00
|
|
|
width: 45px;
|
|
|
|
left: 0;
|
2021-11-29 15:55:05 +01:00
|
|
|
top: 0;
|
2017-12-11 22:30:04 +01:00
|
|
|
text-align: center;
|
2017-12-06 00:42:33 +01:00
|
|
|
display: block;
|
2017-12-11 22:30:04 +01:00
|
|
|
border-bottom: 1px solid;
|
|
|
|
border-right: 1px solid;
|
2018-01-27 18:58:59 +01:00
|
|
|
height: 45px;
|
2016-11-06 21:03:08 +01:00
|
|
|
}
|
|
|
|
|
2019-05-03 00:13:39 +02:00
|
|
|
.rustdoc.source > .sidebar > .sidebar-menu {
|
|
|
|
display: none;
|
|
|
|
}
|
|
|
|
|
2021-07-15 22:06:53 +02:00
|
|
|
/* We do NOT hide this element so that alternative device readers still have this information
|
|
|
|
available. */
|
2017-12-06 00:42:33 +01:00
|
|
|
.sidebar-elems {
|
|
|
|
position: fixed;
|
|
|
|
z-index: 1;
|
|
|
|
top: 45px;
|
|
|
|
bottom: 0;
|
2021-07-15 22:06:53 +02:00
|
|
|
width: 246px;
|
|
|
|
/* We move the sidebar to the left by its own width so it doesn't appear. */
|
|
|
|
left: -246px;
|
2017-12-06 00:42:33 +01:00
|
|
|
overflow-y: auto;
|
2017-12-11 22:30:04 +01:00
|
|
|
border-right: 1px solid;
|
2016-11-06 21:03:08 +01:00
|
|
|
}
|
|
|
|
|
2017-12-11 22:30:04 +01:00
|
|
|
.sidebar > .block.version {
|
2021-06-16 22:24:02 +02:00
|
|
|
overflow: hidden;
|
2017-12-11 22:30:04 +01:00
|
|
|
border-bottom: none;
|
2021-01-05 18:53:23 -05:00
|
|
|
margin-bottom: 0;
|
2021-06-16 22:24:02 +02:00
|
|
|
height: 100%;
|
|
|
|
padding-left: 12px;
|
|
|
|
}
|
|
|
|
.sidebar > .block.version > div.narrow-helper {
|
|
|
|
float: left;
|
|
|
|
width: 1px;
|
|
|
|
height: 100%;
|
|
|
|
}
|
|
|
|
.sidebar > .block.version > p {
|
|
|
|
/* hide Version text if too narrow */
|
|
|
|
margin: 0;
|
|
|
|
min-width: 55px;
|
|
|
|
/* vertically center */
|
|
|
|
display: flex;
|
|
|
|
align-items: center;
|
|
|
|
height: 100%;
|
2017-12-11 22:30:04 +01:00
|
|
|
}
|
|
|
|
|
2021-10-10 00:52:14 +02:00
|
|
|
.source nav:not(.sidebar).sub {
|
|
|
|
margin-left: 32px;
|
|
|
|
}
|
|
|
|
|
2016-11-06 21:03:08 +01:00
|
|
|
.content {
|
|
|
|
margin-left: 0px;
|
|
|
|
}
|
|
|
|
|
2021-10-10 00:52:14 +02:00
|
|
|
.source .content {
|
|
|
|
margin-top: 10px;
|
|
|
|
}
|
|
|
|
|
2017-10-14 15:52:50 +02:00
|
|
|
#search {
|
|
|
|
margin-left: 0;
|
2021-09-30 04:23:02 +02:00
|
|
|
padding: 0;
|
2017-10-14 15:52:50 +02:00
|
|
|
}
|
2017-10-24 22:34:59 +02:00
|
|
|
|
2018-02-19 23:22:08 +03:00
|
|
|
.anchor {
|
2018-02-20 22:46:24 +03:00
|
|
|
display: none !important;
|
2018-02-19 23:22:08 +03:00
|
|
|
}
|
2018-10-06 18:51:56 +02:00
|
|
|
|
2019-04-29 23:43:39 +02:00
|
|
|
.theme-picker {
|
|
|
|
z-index: 1;
|
2016-11-06 21:03:08 +01:00
|
|
|
}
|
2017-11-15 20:04:02 +01:00
|
|
|
|
2021-06-01 21:43:09 -07:00
|
|
|
.notable-traits {
|
2020-07-06 12:53:44 -07:00
|
|
|
position: absolute;
|
|
|
|
left: -22px;
|
|
|
|
top: 24px;
|
|
|
|
}
|
|
|
|
|
2020-12-10 11:38:12 +01:00
|
|
|
#titles > button > div.count {
|
2017-12-18 21:27:19 +01:00
|
|
|
float: left;
|
|
|
|
width: 100%;
|
|
|
|
}
|
|
|
|
|
|
|
|
#titles {
|
|
|
|
height: 50px;
|
|
|
|
}
|
2017-12-20 00:44:44 +01:00
|
|
|
|
2021-07-16 08:04:49 -07:00
|
|
|
.show-it, .sidebar-elems:focus-within {
|
|
|
|
z-index: 2;
|
2021-07-15 22:06:53 +02:00
|
|
|
left: 0;
|
2018-02-04 13:47:35 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
.show-it > .block.items {
|
|
|
|
margin: 8px 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
.show-it > .block.items > ul {
|
|
|
|
margin: 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
.show-it > .block.items > ul > li {
|
|
|
|
text-align: center;
|
|
|
|
margin: 2px 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
.show-it > .block.items > ul > li > a {
|
Set font size proportional to user's font size
According to MDN
(https://developer.mozilla.org/en-US/docs/Web/CSS/font-size),
> To maximize accessibility, it is generally best to use values that
> are relative to the user's default font size.
> Defining font sizes in px is not accessible, because the user cannot
> change the font size in some browsers.
Note that changing font size (in browser or OS settings) is distinct
from the zoom functionality triggered with Ctrl/Cmd-+. Zoom
functionality increases the size of everything on the page, effectively
applying a multiplier to all pixel sizes. Font size changes apply to
just text.
For relative font sizes, we could use `em`, as we do in several places
already. However that has a problem of "compounding" (see MDN article
for details). The compounding problem is nicely solved by `rem`, which
make font sizes relative to the root element, not the parent element.
Since we were using a hodge-podge of pixel sizes, em, rem, and
percentage sizes before, this change switching everything to rem, while
keeping the same size relative to our old default of 16px.
16px is still the default on most browsers, for users that haven't set a
larger or smaller font size.
2021-12-30 16:42:06 -05:00
|
|
|
font-size: 1.3125rem;
|
2017-12-20 00:44:44 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
/* Because of ios, we need to actually have a full height sidebar title so the
|
|
|
|
* actual sidebar can show up. But then we need to make it transparent so we don't
|
|
|
|
* hide content. The filler just allows to create the background for the sidebar
|
|
|
|
* title. But because of the absolute position, I had to lower the z-index.
|
|
|
|
*/
|
|
|
|
#sidebar-filler {
|
|
|
|
position: fixed;
|
|
|
|
left: 45px;
|
|
|
|
width: calc(100% - 45px);
|
|
|
|
top: 0;
|
|
|
|
height: 45px;
|
|
|
|
z-index: -1;
|
|
|
|
border-bottom: 1px solid;
|
|
|
|
}
|
2018-02-17 20:54:00 +03:00
|
|
|
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content > details.rustdoc-toggle > summary::before,
|
|
|
|
#main-content > div > details.rustdoc-toggle > summary::before {
|
2021-05-14 19:58:21 +02:00
|
|
|
left: -11px;
|
2021-04-17 23:43:20 -07:00
|
|
|
}
|
|
|
|
|
2018-10-06 18:51:56 +02:00
|
|
|
#all-types {
|
|
|
|
margin: 10px;
|
|
|
|
}
|
2019-04-29 23:24:09 +02:00
|
|
|
|
2021-10-24 21:59:53 +02:00
|
|
|
.sidebar.expanded #sidebar-toggle {
|
|
|
|
font-size: 1.5rem;
|
|
|
|
}
|
|
|
|
|
|
|
|
.sidebar:not(.expanded) #sidebar-toggle {
|
|
|
|
position: fixed;
|
|
|
|
left: 1px;
|
2019-04-29 23:24:09 +02:00
|
|
|
top: 100px;
|
|
|
|
width: 30px;
|
|
|
|
font-size: 1.5rem;
|
|
|
|
text-align: center;
|
|
|
|
padding: 0;
|
2021-10-24 21:59:53 +02:00
|
|
|
z-index: 10;
|
|
|
|
border-top-right-radius: 3px;
|
|
|
|
border-bottom-right-radius: 3px;
|
|
|
|
cursor: pointer;
|
|
|
|
font-weight: bold;
|
|
|
|
border: 1px solid;
|
|
|
|
border-left: 0;
|
2019-04-29 23:24:09 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
#source-sidebar {
|
|
|
|
z-index: 11;
|
|
|
|
}
|
2019-04-29 23:43:39 +02:00
|
|
|
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content > .line-numbers {
|
2019-04-29 23:43:39 +02:00
|
|
|
margin-top: 0;
|
|
|
|
}
|
2020-07-20 14:37:47 +02:00
|
|
|
|
2020-08-09 12:09:05 -07:00
|
|
|
.notable-traits .notable-traits-tooltiptext {
|
2020-07-20 14:37:47 +02:00
|
|
|
left: 0;
|
|
|
|
top: 100%;
|
|
|
|
}
|
2020-10-15 17:28:42 +02:00
|
|
|
|
|
|
|
/* We don't display the help button on mobile devices. */
|
2021-05-09 11:21:38 -07:00
|
|
|
#help-button {
|
2020-10-15 17:28:42 +02:00
|
|
|
display: none;
|
|
|
|
}
|
2021-05-25 00:36:36 +02:00
|
|
|
|
|
|
|
/* Display an alternating layout on tablets and phones */
|
2021-06-18 00:33:42 +02:00
|
|
|
.item-table {
|
2021-09-12 01:18:39 +02:00
|
|
|
display: block;
|
|
|
|
}
|
|
|
|
.item-row {
|
2021-05-25 00:36:36 +02:00
|
|
|
display: flex;
|
|
|
|
flex-flow: column wrap;
|
|
|
|
}
|
2021-06-18 00:33:42 +02:00
|
|
|
.item-left, .item-right {
|
2021-05-25 00:36:36 +02:00
|
|
|
width: 100%;
|
|
|
|
}
|
|
|
|
|
2020-10-15 17:28:42 +02:00
|
|
|
.search-container > div {
|
|
|
|
width: calc(100% - 32px);
|
|
|
|
}
|
2021-05-21 23:11:06 +02:00
|
|
|
|
|
|
|
/* Display an alternating layout on tablets and phones */
|
|
|
|
.search-results > a {
|
|
|
|
border-bottom: 1px solid #aaa9;
|
2021-05-22 09:01:33 +00:00
|
|
|
padding: 5px 0px;
|
2021-05-21 23:11:06 +02:00
|
|
|
}
|
2021-05-22 16:05:20 +02:00
|
|
|
.search-results .result-name, .search-results div.desc, .search-results .result-description {
|
2021-05-21 23:11:06 +02:00
|
|
|
width: 100%;
|
|
|
|
}
|
2021-06-18 00:33:42 +02:00
|
|
|
.search-results div.desc, .search-results .result-description, .item-right {
|
2021-05-21 23:11:06 +02:00
|
|
|
padding-left: 2em;
|
|
|
|
}
|
2021-12-14 11:48:30 +01:00
|
|
|
|
|
|
|
.source .sidebar.expanded {
|
|
|
|
max-width: 100vw;
|
|
|
|
width: 100vw;
|
|
|
|
}
|
2021-12-29 18:54:33 +01:00
|
|
|
|
|
|
|
/* Position of the "[-]" element. */
|
|
|
|
details.rustdoc-toggle:not(.top-doc) > summary {
|
|
|
|
margin-left: 10px;
|
|
|
|
}
|
|
|
|
.impl-items > details.rustdoc-toggle > summary:not(.hideme)::before,
|
|
|
|
#main-content > details.rustdoc-toggle:not(.top-doc) > summary::before,
|
|
|
|
#main-content > div > details.rustdoc-toggle > summary::before {
|
|
|
|
left: -11px;
|
|
|
|
}
|
2017-12-18 21:27:19 +01:00
|
|
|
}
|
|
|
|
|
2019-04-29 23:43:39 +02:00
|
|
|
@media print {
|
2021-05-11 11:40:26 +02:00
|
|
|
nav.sub, .content .out-of-band {
|
2019-04-29 23:43:39 +02:00
|
|
|
display: none;
|
|
|
|
}
|
|
|
|
}
|
2017-12-18 21:27:19 +01:00
|
|
|
|
2021-01-31 13:42:16 +01:00
|
|
|
@media (max-width: 464px) {
|
2020-12-10 11:38:12 +01:00
|
|
|
#titles, #titles > button {
|
2017-12-18 21:27:19 +01:00
|
|
|
height: 73px;
|
|
|
|
}
|
2020-10-18 21:54:59 +02:00
|
|
|
|
2021-11-29 17:14:05 +01:00
|
|
|
#main-content > table:not(.table-display) td {
|
2020-10-18 21:54:59 +02:00
|
|
|
word-break: break-word;
|
2020-12-11 18:02:23 +01:00
|
|
|
width: 50%;
|
2020-10-18 21:54:59 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
.search-container > div {
|
|
|
|
display: block;
|
|
|
|
width: calc(100% - 37px);
|
|
|
|
}
|
|
|
|
|
|
|
|
#crate-search {
|
|
|
|
border-radius: 4px;
|
|
|
|
border: 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
#theme-picker, #settings-menu {
|
|
|
|
padding: 5px;
|
|
|
|
width: 31px;
|
|
|
|
height: 31px;
|
|
|
|
}
|
|
|
|
|
|
|
|
#theme-picker {
|
|
|
|
margin-top: -2px;
|
|
|
|
}
|
|
|
|
|
|
|
|
#settings-menu {
|
|
|
|
top: 7px;
|
|
|
|
}
|
2021-01-31 01:36:15 +08:00
|
|
|
|
2021-01-31 01:19:29 +08:00
|
|
|
.docblock {
|
|
|
|
margin-left: 12px;
|
|
|
|
}
|
2021-10-07 17:25:58 +02:00
|
|
|
|
|
|
|
.docblock code {
|
2022-01-11 17:36:52 -08:00
|
|
|
overflow-wrap: break-word;
|
2021-10-07 17:25:58 +02:00
|
|
|
overflow-wrap: anywhere;
|
|
|
|
}
|
2021-10-24 22:41:48 +02:00
|
|
|
|
2022-01-11 17:36:52 -08:00
|
|
|
.docblock table code {
|
|
|
|
overflow-wrap: normal;
|
|
|
|
}
|
|
|
|
|
2021-10-24 22:41:48 +02:00
|
|
|
.sub-container {
|
|
|
|
flex-direction: column;
|
|
|
|
}
|
|
|
|
|
|
|
|
.sub-logo-container {
|
|
|
|
align-self: center;
|
|
|
|
}
|
|
|
|
|
|
|
|
.source .sub-logo-container > img {
|
|
|
|
height: 35px;
|
|
|
|
width: 35px;
|
|
|
|
}
|
2021-11-29 15:55:05 +01:00
|
|
|
|
|
|
|
.sidebar:not(.expanded) #sidebar-toggle {
|
|
|
|
top: 10px;
|
|
|
|
}
|
2017-12-08 16:36:08 +01:00
|
|
|
}
|
2021-05-09 16:22:22 -07:00
|
|
|
|
2021-08-26 14:43:12 -07:00
|
|
|
|
|
|
|
/* Begin: styles for --scrape-examples feature */
|
2021-05-09 16:22:22 -07:00
|
|
|
|
2021-08-25 20:15:46 -07:00
|
|
|
.scraped-example-title {
|
|
|
|
font-family: 'Fira Sans';
|
2021-09-14 09:50:47 -07:00
|
|
|
}
|
|
|
|
|
2021-10-07 09:46:18 -07:00
|
|
|
.scraped-example:not(.expanded) .code-wrapper pre.line-numbers {
|
2021-05-09 16:22:22 -07:00
|
|
|
overflow: hidden;
|
2021-08-25 20:15:46 -07:00
|
|
|
max-height: 240px;
|
2021-05-09 16:22:22 -07:00
|
|
|
}
|
|
|
|
|
2021-10-07 09:46:18 -07:00
|
|
|
.scraped-example:not(.expanded) .code-wrapper .example-wrap pre.rust {
|
|
|
|
overflow-y: hidden;
|
|
|
|
max-height: 240px;
|
2021-10-07 10:27:09 -07:00
|
|
|
padding-bottom: 0;
|
2021-10-07 09:46:18 -07:00
|
|
|
}
|
|
|
|
|
2021-05-09 16:22:22 -07:00
|
|
|
.scraped-example .code-wrapper .prev {
|
|
|
|
position: absolute;
|
|
|
|
top: 0.25em;
|
|
|
|
right: 2.25em;
|
|
|
|
z-index: 100;
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example .code-wrapper .next {
|
|
|
|
position: absolute;
|
|
|
|
top: 0.25em;
|
|
|
|
right: 1.25em;
|
|
|
|
z-index: 100;
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example .code-wrapper .expand {
|
|
|
|
position: absolute;
|
|
|
|
top: 0.25em;
|
|
|
|
right: 0.25em;
|
|
|
|
z-index: 100;
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example .code-wrapper {
|
|
|
|
position: relative;
|
|
|
|
display: flex;
|
|
|
|
flex-direction: row;
|
|
|
|
flex-wrap: wrap;
|
|
|
|
width: 100%;
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example:not(.expanded) .code-wrapper:before {
|
|
|
|
content: " ";
|
|
|
|
width: 100%;
|
2021-10-07 09:46:18 -07:00
|
|
|
height: 5px;
|
2021-05-09 16:22:22 -07:00
|
|
|
position: absolute;
|
|
|
|
z-index: 100;
|
|
|
|
top: 0;
|
|
|
|
background: linear-gradient(to bottom, rgba(255, 255, 255, 1), rgba(255, 255, 255, 0));
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example:not(.expanded) .code-wrapper:after {
|
|
|
|
content: " ";
|
|
|
|
width: 100%;
|
2021-10-07 09:46:18 -07:00
|
|
|
height: 5px;
|
2021-05-09 16:22:22 -07:00
|
|
|
position: absolute;
|
|
|
|
z-index: 100;
|
|
|
|
bottom: 0;
|
|
|
|
background: linear-gradient(to top, rgba(255, 255, 255, 1), rgba(255, 255, 255, 0));
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example:not(.expanded) .code-wrapper {
|
|
|
|
overflow: hidden;
|
2021-08-25 20:15:46 -07:00
|
|
|
max-height: 240px;
|
2021-05-09 16:22:22 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example .code-wrapper .line-numbers {
|
|
|
|
margin: 0;
|
|
|
|
padding: 14px 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example .code-wrapper .line-numbers span {
|
|
|
|
padding: 0 14px;
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example .code-wrapper .example-wrap {
|
|
|
|
flex: 1;
|
|
|
|
overflow-x: auto;
|
|
|
|
overflow-y: hidden;
|
|
|
|
margin-bottom: 0;
|
|
|
|
}
|
|
|
|
|
|
|
|
.scraped-example .code-wrapper .example-wrap pre.rust {
|
|
|
|
overflow-x: inherit;
|
|
|
|
width: inherit;
|
|
|
|
overflow-y: hidden;
|
|
|
|
}
|
|
|
|
|
2021-08-26 14:43:12 -07:00
|
|
|
.scraped-example .example-wrap .rust span.highlight {
|
|
|
|
background: #fcffd6;
|
2021-05-09 16:22:22 -07:00
|
|
|
}
|
|
|
|
|
2021-08-26 14:43:12 -07:00
|
|
|
.scraped-example .example-wrap .rust span.highlight.focus {
|
2021-05-09 16:22:22 -07:00
|
|
|
background: #f6fdb0;
|
|
|
|
}
|
|
|
|
|
2021-10-06 21:43:40 -07:00
|
|
|
.more-examples-toggle {
|
|
|
|
margin-top: 10px;
|
|
|
|
}
|
|
|
|
|
2021-06-01 14:02:09 -07:00
|
|
|
.more-examples-toggle summary {
|
|
|
|
color: #999;
|
2021-08-26 14:43:12 -07:00
|
|
|
font-family: 'Fira Sans';
|
2021-06-01 14:02:09 -07:00
|
|
|
}
|
|
|
|
|
2021-05-09 16:22:22 -07:00
|
|
|
.more-scraped-examples {
|
2021-09-13 18:08:14 -07:00
|
|
|
margin-left: 25px;
|
2021-08-25 20:15:46 -07:00
|
|
|
display: flex;
|
|
|
|
flex-direction: row;
|
2021-09-13 18:08:14 -07:00
|
|
|
width: calc(100% - 25px);
|
|
|
|
}
|
|
|
|
|
|
|
|
.more-scraped-examples-inner {
|
|
|
|
/* 20px is width of toggle-line + toggle-line-inner */
|
|
|
|
width: calc(100% - 20px);
|
2021-08-25 20:15:46 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
.toggle-line {
|
|
|
|
align-self: stretch;
|
|
|
|
margin-right: 10px;
|
|
|
|
margin-top: 5px;
|
|
|
|
padding: 0 4px;
|
|
|
|
cursor: pointer;
|
|
|
|
}
|
|
|
|
|
|
|
|
.toggle-line:hover .toggle-line-inner {
|
|
|
|
background: #aaa;
|
|
|
|
}
|
|
|
|
|
|
|
|
.toggle-line-inner {
|
|
|
|
min-width: 2px;
|
|
|
|
background: #ddd;
|
|
|
|
height: 100%;
|
|
|
|
}
|
|
|
|
|
|
|
|
.more-scraped-examples .scraped-example {
|
|
|
|
margin-bottom: 20px;
|
|
|
|
}
|
|
|
|
|
2021-09-14 09:50:47 -07:00
|
|
|
.more-scraped-examples .scraped-example:last-child {
|
|
|
|
margin-bottom: 0;
|
|
|
|
}
|
|
|
|
|
2021-08-25 20:15:46 -07:00
|
|
|
.example-links a {
|
2021-09-14 09:50:47 -07:00
|
|
|
margin-top: 20px;
|
2021-08-25 20:15:46 -07:00
|
|
|
font-family: 'Fira Sans';
|
|
|
|
}
|
|
|
|
|
|
|
|
.example-links ul {
|
|
|
|
margin-bottom: 0;
|
2021-05-09 16:22:22 -07:00
|
|
|
}
|
2021-08-26 14:43:12 -07:00
|
|
|
|
|
|
|
/* End: styles for --scrape-examples feature */
|