diff --git a/src/verso-blog/Verso/Genre/Blog/Template.lean b/src/verso-blog/Verso/Genre/Blog/Template.lean index a2ec6c2..b3f3af1 100644 --- a/src/verso-blog/Verso/Genre/Blog/Template.lean +++ b/src/verso-blog/Verso/Genre/Blog/Template.lean @@ -141,6 +141,58 @@ def _root_.Array.mapIndexed (arr : Array α) (f : Fin arr.size → α → β) : termination_by arr.size - i go #[] 0 +partial defmethod Highlighted.isEmpty (hl : Highlighted) : Bool := + match hl with + | .text str => str.isEmpty + | .token .. => false + | .span _ _ hl => hl.isEmpty + | .tactics _ _ hl => hl.isEmpty + | .point .. => true + | .seq hls => hls.all isEmpty + +partial defmethod Highlighted.trimRight (hl : Highlighted) : Highlighted := + match hl with + | .text str => .text str.trimRight + | .token .. => hl + | .span s info hl => .span s info hl.trimRight + | .tactics info pos hl => .tactics info pos hl.trimRight + | .point .. => hl + | .seq hls => Id.run do + let mut hls := hls + repeat + if h : hls.size > 0 then + have : hls.size - 1 < hls.size := by + apply Nat.sub_lt_of_pos_le + . simp + . exact h + if hls[hls.size - 1].isEmpty then + hls := hls.pop + else break + else break + if h : hls.size > 0 then + let i := hls.size - 1 + have : i < hls.size := by + dsimp (config := {zetaDelta := true}) + apply Nat.sub_lt_of_pos_le + . simp + . exact h + --dbg_trace repr hls[i] + .seq <| hls.set ⟨i, by assumption⟩ hls[i].trimRight + else hl + +partial defmethod Highlighted.trimLeft (hl : Highlighted) : Highlighted := + match hl with + | .text str => .text str.trimLeft + | .token .. => hl + | .span s info hl => .span s info hl.trimLeft + | .tactics info pos hl => .tactics info pos hl.trimLeft + | .point .. => hl + | .seq hls => + if h : hls.size > 0 then + .seq <| hls.set ⟨0, h⟩ hls[0].trimLeft + else hl + +defmethod Highlighted.trim (hl : Highlighted) : Highlighted := hl.trimLeft.trimRight partial defmethod Highlighted.toHtml : Highlighted → Html | .token t => t.toHtml @@ -169,7 +221,7 @@ def blockHtml (g : Genre) (go : Block g → HtmlT g IO Html) : Blog.BlockExt → | .lexedText content, _contents => do pure {{
{{ content.toHtml }}}} | .highlightedCode contextName hls, _contents => do - pure {{
{{ hls.toHtml }}
}}
+ pure {{ {{ hls.trim.toHtml }}
}}
| .htmlDetails classes summary, contents => do
pure {{ {{ hls.toHtml }}
}}
+ pure {{ {{ hls.trim.toHtml }}
}}
| .customHighlight hls, _contents => do
- pure {{ {{ hls.toHtml }}
}}
+ pure {{ {{ hls.trim.toHtml }}
}}
| .label x, contents => do
let contentHtml ← contents.mapM go
let st ← stateEq ▸ state
diff --git a/src/verso/Verso/Output/Html.lean b/src/verso/Verso/Output/Html.lean
index 41756ca..7252980 100644
--- a/src/verso/Verso/Output/Html.lean
+++ b/src/verso/Verso/Output/Html.lean
@@ -245,11 +245,11 @@ partial def asString (html : Html) (indent : Nat := 0) (breakLines := true) : St
| .tag "pre" attrs body =>
"" ++ Html.asString (indent := 0) (breakLines := false) body ++ - "" ++ newline indent + "" ++ breakline "pre" | .tag "code" attrs body => "
" ++
Html.asString (indent := 0) (breakLines := false) body ++
- "
" ++ newline indent
+ "" ++ breakline "code"
| .tag name attrs (.seq #[]) =>
if name ∈ mustClose then
"<" ++ name ++ attrsAsString attrs ++ ">" ++ name ++ ">" ++ breakline name