From ec23b215b46564f55ee200003c53abe74c426ef2 Mon Sep 17 00:00:00 2001 From: John Merkel Date: Thu, 15 Feb 2024 10:35:38 -0800 Subject: [PATCH 1/3] Add css for `
` / `` Follow up from: https://github.com/JuliaPluto/PlutoUI.jl/pull/288#pullrequestreview-1880829370 --- frontend/editor.css | 53 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/frontend/editor.css b/frontend/editor.css index 4a2407741f..f90308ae34 100644 --- a/frontend/editor.css +++ b/frontend/editor.css @@ -465,6 +465,59 @@ pluto-output mjx-assistive-mml { overflow: hidden; } +pluto-output details { + border: 1px solid var(--rule-color); + border-radius: 4px; + padding: 0.5em 0.5em 0; + margin-block-start: 0; + margin-block-end: var(--pluto-cell-spacing); +} + +pluto-output details:first-child { + margin-block-start: 0; +} + +pluto-output details:last-child { + margin-block-end: 0; +} + +pluto-output details summary { + cursor: pointer; + font-family: var(--system-ui-font-stack); + font-weight: bold; + border-radius: 3px; + padding: 0.5em; + margin: -0.5em -0.5em 0; + transition: color .25s ease-in-out, background-color .25s ease-in-out; + /* Border may have transparency, let's not change the border with a background-color */ + background-clip: padding-box; +} + +pluto-output details summary:hover { + color: var(--blockquote-color); + background-color: var(--blockquote-bg); +} + +pluto-output details[open] { + padding: 0.5em; +} + +pluto-output details[open] summary { + border-bottom: 1px solid var(--rule-color); + border-bottom-right-radius: 0; + border-bottom-left-radius: 0; + margin-bottom: 0.5em; +} + +pluto-output details plutoui-detail { + display: block; + margin-block-end: var(--pluto-cell-spacing); +} + +pluto-output details plutoui-detail:last-child { + margin-block-end: 0; +} + /* HEADER */ header#pluto-nav { From 7190826c1155a94773167f9fadae734a0ad4cb86 Mon Sep 17 00:00:00 2001 From: John Merkel Date: Fri, 16 Feb 2024 10:55:00 -0800 Subject: [PATCH 2/3] Repalce accidental tab with space indenting --- frontend/editor.css | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontend/editor.css b/frontend/editor.css index f90308ae34..0c6e18d9a1 100644 --- a/frontend/editor.css +++ b/frontend/editor.css @@ -482,7 +482,7 @@ pluto-output details:last-child { } pluto-output details summary { - cursor: pointer; + cursor: pointer; font-family: var(--system-ui-font-stack); font-weight: bold; border-radius: 3px; From c7a8ab126bd864323ffb3fccdf9f082ed5ad036f Mon Sep 17 00:00:00 2001 From: Fons van der Plas Date: Sun, 18 Feb 2024 09:48:17 +0100 Subject: [PATCH 3/3] remove plutoui specific styles --- frontend/editor.css | 9 --------- 1 file changed, 9 deletions(-) diff --git a/frontend/editor.css b/frontend/editor.css index 0c6e18d9a1..89dd0d4214 100644 --- a/frontend/editor.css +++ b/frontend/editor.css @@ -509,15 +509,6 @@ pluto-output details[open] summary { margin-bottom: 0.5em; } -pluto-output details plutoui-detail { - display: block; - margin-block-end: var(--pluto-cell-spacing); -} - -pluto-output details plutoui-detail:last-child { - margin-block-end: 0; -} - /* HEADER */ header#pluto-nav {