feat: mod doc heading attributes
parent
385a38a003
commit
d3ce268d63
|
@ -11,6 +11,7 @@ import DocGen4.Output.Class
|
||||||
import DocGen4.Output.Definition
|
import DocGen4.Output.Definition
|
||||||
import DocGen4.Output.Instance
|
import DocGen4.Output.Instance
|
||||||
import DocGen4.Output.ClassInductive
|
import DocGen4.Output.ClassInductive
|
||||||
|
import Lean.Data.Xml.Parser
|
||||||
|
|
||||||
namespace DocGen4
|
namespace DocGen4
|
||||||
namespace Output
|
namespace Output
|
||||||
|
@ -102,11 +103,41 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
|
||||||
</div>
|
</div>
|
||||||
</div>
|
</div>
|
||||||
|
|
||||||
|
open Xml in
|
||||||
|
partial def addAttributes : Element → Element
|
||||||
|
| (Element.Element name attrs contents) =>
|
||||||
|
if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then
|
||||||
|
let id := "".intercalate (contents.map toString).toList
|
||||||
|
|>.dropWhile (λ c => !(c.isAlphanum ∨ c = '-'))
|
||||||
|
|>.toLower
|
||||||
|
|>.replace " " "-"
|
||||||
|
let anchorAttributes := Std.RBMap.empty
|
||||||
|
|>.insert "class" "hover-link"
|
||||||
|
|>.insert "href" s!"#{id}"
|
||||||
|
let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
|
||||||
|
let newAttrs := attrs
|
||||||
|
|>.insert "id" id
|
||||||
|
|>.insert "class" "markdown-heading"
|
||||||
|
let newContents := contents.map (λ c => match c with
|
||||||
|
| Content.Element e => Content.Element (addAttributes e)
|
||||||
|
| _ => c)
|
||||||
|
|>.push (Content.Element anchor)
|
||||||
|
⟨ name, newAttrs, newContents⟩
|
||||||
|
else
|
||||||
|
let newContents := contents.map λ c => match c with
|
||||||
|
| Content.Element e => Content.Element (addAttributes e)
|
||||||
|
| _ => c
|
||||||
|
⟨ name, attrs, newContents⟩
|
||||||
|
|
||||||
def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
|
def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
|
||||||
pure
|
let rendered := toString
|
||||||
<div «class»="mod_doc">
|
<div «class»="mod_doc">
|
||||||
{Html.text (CMark.renderHtml mdoc.doc)}
|
{Html.text (CMark.renderHtml mdoc.doc)}
|
||||||
</div>
|
</div>
|
||||||
|
let modified := match Lean.Xml.parse rendered with
|
||||||
|
| Except.ok parsed => toString $ addAttributes parsed
|
||||||
|
| _ => rendered
|
||||||
|
pure (Html.text modified)
|
||||||
|
|
||||||
def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html :=
|
def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html :=
|
||||||
match member with
|
match member with
|
||||||
|
|
Loading…
Reference in New Issue