From 18b1739b890b4659d936b80e17ccce74ffb1952e Mon Sep 17 00:00:00 2001 From: Aria Date: Tue, 26 Aug 2025 12:53:38 -0500 Subject: [PATCH] Add a space after paragraphs in descriptions and add padding to hover tooltips --- website/src/repl/Repl.css | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/website/src/repl/Repl.css b/website/src/repl/Repl.css index b8443081f..b74eff218 100644 --- a/website/src/repl/Repl.css +++ b/website/src/repl/Repl.css @@ -72,8 +72,7 @@ /* Override default styles from the codemirror inline css for autocomplete info tooltip*/ .cm-tooltip.cm-completionInfo { - padding: 12px !important; - padding-bottom: 12px !important; + padding: 0 !important; border: 1px solid var(--foreground) !important; border-radius: 4px !important; box-shadow: 0 4px 12px rgba(0, 0, 0, 0.3) !important; @@ -87,6 +86,8 @@ /* Main tooltip container */ .autocomplete-info-tooltip { + padding: 12px !important; + padding-bottom: 12px !important; border-radius: 4px !important; color: var(--foreground); font-family: var(--font-family, 'SF Mono', 'Monaco', monospace); @@ -97,6 +98,10 @@ min-width: 400px; } +.autocomplete-info-tooltip p { + margin-bottom: 1em; +} + .autocomplete-info-function-name { font-size: 15px; font-weight: 600;