Merge pull request #4504 from roc-lang/fix-styles

Fix some web styles
This commit is contained in:
Richard Feldman 2022-11-16 21:53:05 -05:00 committed by GitHub
commit 1e4cf52fd4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 38 additions and 4 deletions

View File

@ -468,6 +468,12 @@ pre {
line-height: 15px;
}
.builtins-tip {
padding: 1em;
font-style: italic;
line-height: 1.3em;
}
@media (prefers-color-scheme: dark) {
:root {
--body-bg-color: var(--purple-8);

View File

@ -275,7 +275,7 @@ pub const ANSI_STYLE_CODES: StyleCodes = StyleCodes {
macro_rules! html_color {
($name: expr) => {
concat!("<span style='color: ", $name, "'>")
concat!("<span class='color-", $name, "'>")
};
}
@ -287,8 +287,8 @@ pub const HTML_STYLE_CODES: StyleCodes = StyleCodes {
magenta: html_color!("magenta"),
cyan: html_color!("cyan"),
white: html_color!("white"),
bold: "<span style='font-weight: bold'>",
underline: "<span style='text-decoration: underline'>",
bold: "<span class='bold'>",
underline: "<span class='underline'>",
reset: "</span>",
color_reset: "</span>",
};

View File

@ -56,7 +56,7 @@ mv generated-docs/*.* www/build # move all the .js, .css, etc. files to build/
mv generated-docs/ www/build/builtins # move all the folders to build/builtins/
# Manually add this tip to all the builtin docs.
find www/build/builtins -type f -name 'index.html' -exec sed -i 's!</nav>!<div style="padding: 1em;font-style: italic;line-height: 1.3em;"><strong>Tip:</strong> <a href="/different-names">Some names</a> differ from other languages.</div></nav>!' {} \;
find www/build/builtins -type f -name 'index.html' -exec sed -i 's!</nav>!<div class="builtins-tip"><b>Tip:</b> <a href="/different-names">Some names</a> differ from other languages.</div></nav>!' {} \;
echo 'Generating CLI example platform docs...'
# Change ROC_DOCS_ROOT_DIR=builtins so that links will be generated relative to

View File

@ -75,3 +75,31 @@ section.source textarea {
padding: 8px;
margin-bottom: 16px;
}
.color-red {
color: red;
}
.color-green {
color: green;
}
.color-yellow {
color: yellow;
}
.color-blue {
color: blue;
}
.color-magenta {
color: magenta;
}
.color-cyan {
color: cyan;
}
.color-white {
color: white;
}
.bold {
font-weight: bold;
}
.underline {
text-decoration: underline;
}