r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

feat: html escape docstrings

main
Alex J. Best 2023-10-16 17:27:36 +01:00 committed by Henrik Böving
parent f9d9875671
commit 074c783259
2 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
DocGen4/Output/DocString.lean
View File

@ -210,11 +210,11 @@ partial def modifyElement (element : Element) : HtmlM Element :=
/-- Convert docstring to Html. -/ /-- Convert docstring to Html. -/
def docStringToHtml (s : String) : HtmlM (Array Html) := do def docStringToHtml (s : String) : HtmlM (Array Html) := do
let rendered := CMark.renderHtml s let rendered := CMark.renderHtml (Html.escape s)
match manyDocument rendered.mkIterator with match manyDocument rendered.mkIterator with
| Parsec.ParseResult.success _ res => | Parsec.ParseResult.success _ res =>
res.mapM fun x => do return Html.text <| toString (← modifyElement x) res.mapM fun x => do return Html.text <| toString (← modifyElement x)
| _ => return #[Html.text rendered] | _ => return #[Html.text <| rendered]
end Output end Output
end DocGen4 end DocGen4

8
DocGen4/Output/ToHtmlFormat.lean
View File

@ -53,10 +53,10 @@ partial def textLength : Html → Nat
def escapePairs : Array (String × String) := def escapePairs : Array (String × String) :=
#[ #[
("&", "&amp"), ("&", "&amp;"),
("<", "&lt"), ("<", "&lt;"),
(">", "&gt"), (">", "&gt;"),
("\"", "&quot") ("\"", "&quot;")
] ]
def escape (s : String) : String := def escape (s : String) : String :=