]> gitweb.factorcode.org Git - factor.git/commitdiff
help.stylesheet: giving code blocks a border color
authorJohn Benediktsson <mrjbq7@gmail.com>
Mon, 25 Jul 2022 21:17:05 +0000 (14:17 -0700)
committerJohn Benediktsson <mrjbq7@gmail.com>
Mon, 25 Jul 2022 21:17:05 +0000 (14:17 -0700)
basis/help/stylesheet/stylesheet.factor
basis/ui/theme/switching/tools/tools.factor
basis/ui/theme/theme.factor

index 5935c0379b98608f78877ffeeb312c1673a50d15..7f858c252d90a2b506d1dcefd43b8573a02657c5 100644 (file)
@@ -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
index 1a56b83fd546d7b40bcd2978ab843ce6046fc8e7..f10a07fd11a4ea4d37cdb3463224b87ce3db1fcf 100644 (file)
@@ -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
index d04d2a0981dd1be1afdf4ca39dc309e16fcc809e..54d501e8680e6187de7b670085ffd3ee4af8e9e0 100644 (file)
@@ -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 ;