From 267c6c46d9684ba4a5ee54269059c9119930e12a Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 18 Dec 2024 17:42:57 +0100 Subject: [PATCH 1/6] css: Reduce font size for the sidebar top-level item This item was comically large and overflowed easily. --- src/html_support_files/odoc.css | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index 2f0dd6c741..e5248cab4f 100644 --- a/src/html_support_files/odoc.css +++ b/src/html_support_files/odoc.css @@ -930,7 +930,6 @@ body.odoc:has( .odoc-search) .odoc-toc { .odoc-toc.odoc-global-toc > ul > li > ul > li { font-weight: 500; - font-size: 500; } .odoc-toc.odoc-global-toc > ul > li > ul > li > a { @@ -939,7 +938,7 @@ body.odoc:has( .odoc-search) .odoc-toc { } .odoc-toc.odoc-global-toc > ul > li > a { - font-size: 2em; + font-size: 1.2em; } .current_unit { From 0ddc5f01175cce0570eefa069e3de09827d29707 Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 18 Dec 2024 17:56:16 +0100 Subject: [PATCH 2/6] css: Tweak current unit highlight in sidebar Use the same style as targetted headings. --- src/html_support_files/odoc.css | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index e5248cab4f..d204968e1f 100644 --- a/src/html_support_files/odoc.css +++ b/src/html_support_files/odoc.css @@ -460,7 +460,7 @@ a:hover:not(.img-link) { } /* Linked highlight */ -*:target { +*:target, .current_unit { background-color: var(--target-background) !important; border-radius: 1px; border: var(--target-border) 1px solid !important; @@ -941,10 +941,6 @@ body.odoc:has( .odoc-search) .odoc-toc { font-size: 1.2em; } -.current_unit { - background-color: var(--anchor-color); -} - :root { --search-bar-height: 25px; --search-padding-top: 1rem; From fd45c3101a1ff91a10a96a62ca2db3c3f436c027 Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 18 Dec 2024 17:56:50 +0100 Subject: [PATCH 3/6] css: Unindent local content sidebar Items are often long enough to break. --- src/html_support_files/odoc.css | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index d204968e1f..903bce09cb 100644 --- a/src/html_support_files/odoc.css +++ b/src/html_support_files/odoc.css @@ -1234,7 +1234,7 @@ body.odoc:has( .odoc-search) .odoc-toc { font-weight: 500; } -.odoc-toc li ul { +.odoc-toc ul li ul { margin: 0px; padding-top: 0.25em; } @@ -1248,6 +1248,7 @@ body.odoc:has( .odoc-search) .odoc-toc { } .odoc-toc>ul>li { + margin-left: 0; margin-bottom: 0.3em; } From be8f1aacfe7f93d5afba31f06c3b8353d97ec3d1 Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 18 Dec 2024 18:14:46 +0100 Subject: [PATCH 4/6] css: Reduce margin after title when no preamble This margin was noticeable in source code pages. --- src/html_support_files/odoc.css | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index 903bce09cb..0d7bf0acf5 100644 --- a/src/html_support_files/odoc.css +++ b/src/html_support_files/odoc.css @@ -364,7 +364,8 @@ body.odoc-src { margin-top: 0; } -header { +/* Add margin after the preamble if it contains more than one element. */ +header.odoc-preamble:has(> :nth-child(2)) { margin-bottom: 30px; } From a9e71122d2e2f1fa93a7bc958224cb8f067d3b75 Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 18 Dec 2024 18:15:50 +0100 Subject: [PATCH 5/6] css: Reduce margin above source code pages --- src/html_support_files/odoc.css | 1 + 1 file changed, 1 insertion(+) diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index 0d7bf0acf5..64478369e2 100644 --- a/src/html_support_files/odoc.css +++ b/src/html_support_files/odoc.css @@ -1372,6 +1372,7 @@ body.odoc:has( .odoc-search) .odoc-toc { .source_container { display: flex; grid-area: content; + margin-top: 0; } .source_line_column { From 438b348218b9d577f4bfa5891234e005c2e92f10 Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 18 Dec 2024 18:16:06 +0100 Subject: [PATCH 6/6] css: Tweak number line color in source code pages --- src/html_support_files/odoc.css | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index 64478369e2..9fc310a982 100644 --- a/src/html_support_files/odoc.css +++ b/src/html_support_files/odoc.css @@ -230,7 +230,7 @@ --source-line-column: var(--fg3); - --source-line-column-bg: var(--bg1); + --source-line-column-bg: var(--bg_h); --source-code-comment: var(--gray); --source-code-docstring: var(--green-dim);