]> gitweb.factorcode.org Git - factor.git/commitdiff
help.html: trying a lightweight theme
authorJohn Benediktsson <mrjbq7@gmail.com>
Tue, 11 Jan 2022 23:51:39 +0000 (15:51 -0800)
committerJohn Benediktsson <mrjbq7@gmail.com>
Tue, 11 Jan 2022 23:51:39 +0000 (15:51 -0800)
basis/help/html/html.factor
basis/help/html/stylesheet.css

index 014eaa32460f30a6b5e3120112e2eb35b591e9ab..aa846023e3f9c2cd2812b42c1ccd389eb58c6e3d 100644 (file)
@@ -95,8 +95,8 @@ M: pathname url-of
 : help-footer ( -- xml )
     version-info "\n" split1 drop
     [XML
-        <br />
-        <p style="color: #666; font-size: smaller;">
+        <div class="footer">
+        <p>
         This documentation was generated offline from a
         <code>load-all</code> image.  If you want, you can also
         browse the documentation from within the <a
@@ -104,7 +104,8 @@ M: pathname url-of
         the <a href="https://factorcode.org">Factor website</a>
         for more information.
         </p>
-        <p style="color: #666; font-size: smaller;"><-></p>
+        <p><-></p>
+        </div>
     XML] ;
 
 : bijective-base26 ( n -- name )
@@ -138,11 +139,13 @@ M: pathname url-of
     dup [
         [ ".a" head? ] [ "#f4efd9;" swap subseq? ] bi and
     ] find [
-        "padding: 10px;" "padding: 15px;" replace
+        "padding: 10px;" "padding: 0px;" replace
+        "background-color: #f4efd9;" "background-color: white;" replace
         "}" ?tail drop
-        " border-bottom: 1px solid #ccc; width: calc(100% + 30px); margin: -15px; }"
+        " border-bottom: 1px dashed #ccc; width: 100%; padding-bottom: 10px; }"
         append swap pick set-nth
-        ".a tr:hover { background-color: #f4efd9; }" prefix
+        ".a tr:hover { background-color: white; }" prefix
+        ".a td { border: none; }" prefix
     ] [ drop ] if* ;
 
 : css-classes ( classes -- stylesheet )
index 74a313874b5d3f5735366c75cbf9426eb77142c9..b9c866a1a928cf18dcf02ac46ae0b2a4667695e7 100644 (file)
@@ -73,6 +73,13 @@ tr:hover {
     height: 16px;
 }
 
+.footer {
+    margin-top: 15px;
+    border-top: 1px dashed #ccc;
+    color: #666;
+    font-size: smaller;
+}
+
 @media screen and (max-width: 480px) {
 
     input {