Fix softbreak rendering

This commit is contained in:
Nathan McCarty 2025-02-21 05:47:46 -05:00
parent 67a07a0523
commit 72418a0b88

View file

@ -7,24 +7,27 @@ import SSG.Djot.Block
import Data.String
import Data.List1
import Data.List
import Structures.Dependent.DList
-- Maybe because specifically Soft line breaks don't generate any html of their
-- own
export
renderInline : Inline -> (type : String ** Html type)
renderInline : Inline -> Maybe (type : String ** Html type)
renderInline HardLineBreak =
(_ ** Void "br" [])
Just (_ ** Void "br" [])
renderInline SoftLineBreak =
(_ ** Text "\n")
Nothing
renderInline NonBreakingSpace =
(_ ** Text " ")
Just (_ ** Text " ")
renderInline (Text c) =
(_ ** Text c)
Just (_ ** Text c)
export
renderInlines : List Inline -> (types : List String ** DList _ Html types)
renderInlines xs =
fromList . map renderInline $ xs
fromList . catMaybes . map renderInline $ xs
headingLevel : HeaderLevel -> (h : String ** IsNormal h)
headingLevel H1 = ("h1" ** IsH1)