From: John Benediktsson <mrjbq7@gmail.com>
Date: Mon, 25 Jul 2022 21:17:05 +0000 (-0700)
Subject: help.stylesheet: giving code blocks a border color
X-Git-Tag: 0.99~1333
X-Git-Url: https://gitweb.factorcode.org/gitweb.cgi?p=factor.git;a=commitdiff_plain;h=cac3c968f1ecdcfe651de2ce8c7afc8c6abfc363

help.stylesheet: giving code blocks a border color
---

diff --git a/basis/help/stylesheet/stylesheet.factor b/basis/help/stylesheet/stylesheet.factor
index 5935c0379b..7f858c252d 100644
--- a/basis/help/stylesheet/stylesheet.factor
+++ b/basis/help/stylesheet/stylesheet.factor
@@ -94,6 +94,7 @@ H{
     { font-size $ default-font-size }
     { foreground $ text-color }
     { page-color $ code-background-color }
+    { border-color $ code-border-color }
     { inset { 5 5 } }
     { wrap-margin f }
 } code-style set-global
diff --git a/basis/ui/theme/switching/tools/tools.factor b/basis/ui/theme/switching/tools/tools.factor
index 1a56b83fd5..f10a07fd11 100644
--- a/basis/ui/theme/switching/tools/tools.factor
+++ b/basis/ui/theme/switching/tools/tools.factor
@@ -19,6 +19,7 @@ IN: ui.theme.switching.tools
     heading-style heading-color foreground update-style
     snippet-style snippet-color foreground update-style
     code-style code-background-color page-color update-style
+    code-style code-border-color border-color update-style
     code-style text-color foreground update-style
     output-style output-color foreground update-style
     url-style link-color foreground update-style
diff --git a/basis/ui/theme/theme.factor b/basis/ui/theme/theme.factor
index d04d2a0981..54d501e868 100644
--- a/basis/ui/theme/theme.factor
+++ b/basis/ui/theme/theme.factor
@@ -67,6 +67,7 @@ HOOK: deprecated-border-color theme ( -- color )
 HOOK: warning-background-color theme ( -- color )
 HOOK: warning-border-color theme ( -- color )
 HOOK: code-background-color theme ( -- color )
+HOOK: code-border-color theme ( -- color )
 HOOK: help-path-border-color theme ( -- color )
 
 HOOK: tip-background-color theme ( -- color )
@@ -157,6 +158,7 @@ M: light-theme deprecated-border-color COLOR: #F37B00 ;
 M: light-theme warning-background-color COLOR: #F4D9D9 ;
 M: light-theme warning-border-color COLOR: #F42300 ;
 M: light-theme code-background-color COLOR: FactorLightTan ;
+M: light-theme code-border-color COLOR: FactorTan ;
 M: light-theme help-path-border-color COLOR: grey95 ;
 
 M: light-theme tip-background-color COLOR: lavender ;
@@ -246,6 +248,7 @@ M: dark-theme deprecated-border-color COLOR: solarized-yellow ;
 M: dark-theme warning-background-color COLOR: #492d33 ;
 M: dark-theme warning-border-color COLOR: solarized-red ;
 M: dark-theme code-background-color COLOR: #2F4D5B ;
+M: dark-theme code-border-color COLOR: #666666 ;
 M: dark-theme help-path-border-color COLOR: solarized-base02 ;
 
 M: dark-theme tip-background-color COLOR: #2F4D5B ;