From 72418a0b8897e9a365ca5e119b5c7f2be023a3c4 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 05:47:46 -0500 Subject: [PATCH] Fix softbreak rendering --- src/SSG/Djot/Render.idr | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index 4daf1ce..bffca50 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -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)