From 0490b3de98322d7c3e830e059ff1d9d93c6af7f0 Mon Sep 17 00:00:00 2001 From: Johann Rudloff Date: Sun, 2 May 2021 22:54:22 +0200 Subject: [PATCH] [ docs ] Fix operators and docstrings not being HTML-escaped --- src/Idris/Doc/HTML.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Idris/Doc/HTML.idr b/src/Idris/Doc/HTML.idr index eaa89810b..c313eff0b 100644 --- a/src/Idris/Doc/HTML.idr +++ b/src/Idris/Doc/HTML.idr @@ -44,7 +44,7 @@ packageInternal _ = pure False prettyNameRoot : Name -> String prettyNameRoot n = - let root = nameRoot n in + let root = htmlEscape $ nameRoot n in if isOpName n then "(" ++ root ++ ")" else root renderHtml : {auto c : Ref Ctxt Defs} -> @@ -53,7 +53,7 @@ renderHtml : {auto c : Ref Ctxt Defs} -> renderHtml STEmpty = pure neutral renderHtml (STChar ' ') = pure " " renderHtml (STChar c) = pure $ cast c -renderHtml (STText _ text) = pure text +renderHtml (STText _ text) = pure $ htmlEscape text renderHtml (STLine _) = pure "
" renderHtml (STAnn Declarations rest) = pure $ "
" <+> !(renderHtml rest) <+> "
" renderHtml (STAnn (Decl n) rest) = pure $ "
" <+> !(renderHtml rest) <+> "
"