]> gitweb.factorcode.org Git - factor.git/commitdiff
help.html: more default html output
authorJohn Benediktsson <mrjbq7@gmail.com>
Tue, 31 Jan 2023 19:40:46 +0000 (11:40 -0800)
committerJohn Benediktsson <mrjbq7@gmail.com>
Tue, 31 Jan 2023 19:41:06 +0000 (11:41 -0800)
basis/help/html/html.factor
basis/help/html/stylesheet.css

index 6a5e7f84d4bedbe67f90d6f636a3186875fc909c..d02f3d8b7cbec843944d15318a5f90aff25ad053 100644 (file)
@@ -172,10 +172,6 @@ M: pathname url-of
         " width: fit-content; white-space: pre-wrap; line-height: 125%;" append
     ] re-replace-with
 
-    dup { "font-family: monospace;" "background-color:" } [ subseq-of? ] with all? [
-        " margin: 1.0rem 0;" append
-    ] when
-
     dup { "border:" "background-color:" } [ subseq-of? ] with all? [
         " border-radius: 5px;" append
     ] when ;
@@ -277,26 +273,8 @@ M: pathname url-of
         [XML <-><div class="page"><-><-></div> XML]
     ] bi simple-page ;
 
-: fix-spacing ( html -- html' )
-    ! one line spacing before/after divs
-    "div><br/><br/><" "div><br/><" replace
-    "><br/><br/><div" "><br/><div" replace
-
-    ! one line spacing before after tables
-    "table><br/><br/><" "table><br/><" replace
-    "><br/><br/><table" "><br/><table" replace
-
-    ! spans before or after divs don't need line breaks
-    "span><br/><div" "span><div" replace
-    "div><br/><span" "div><span" replace
-
-    ! spans before or after tables don't need line breaks
-    "span><br/><table" "span><table" replace
-    "table><br/><span" "table><span" replace ;
-
 : generate-help-file ( topic -- )
-    [ help>html xml>string fix-spacing ]
-    [ topic>filename utf8 set-file-contents ] bi ;
+    dup topic>filename utf8 [ help>html write-xml ] with-file-writer ;
 
 : all-vocabs-really ( -- seq )
     all-disk-vocabs-recursive filter-vocabs
index 4969051b5b92c51a19875d55a7448b08b6e9ad36..20f7d0007c1024f4f3d100798f5e79aa8fa6c373 100644 (file)
@@ -75,14 +75,6 @@ nav input {
     height: 16px;
 }
 
-.page div:not(.a) {
-    width: fit-content;
-}
-
-.page div:not(.a) table {
-    margin: 1.0rem 0;
-}
-
 footer {
     margin-top: 15px;
     border-top: 1px dashed #d5d5d5;