main
Alex J. Best 2022-11-05 18:46:20 +01:00
parent 07cb0ed1cc
commit d62268b013
1 changed files with 3 additions and 1 deletions

View File

@ -188,7 +188,9 @@ partial def modifyElement (element : Element) : HtmlM Element :=
else if name = "a" then else if name = "a" then
extendAnchor el extendAnchor el
-- auto link for inline <code></code> -- auto link for inline <code></code>
else if name = "code" ∧ attrs.find? "class" = "language-lean" then else if name = "code" ∧
-- don't linkify code blocks explicitly tagged with a language other than lean
((¬ attrs.contains "class") (((attrs.find? "class").getD "").splitOn).filter (fun s => s.startsWith "language-" ∧ s ≠ "language-lean") = []) then
autoLink el autoLink el
-- recursively modify -- recursively modify
else else