idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-29 03:24:02 +03:00
Code Issues Projects Releases Wiki Activity

[ docs ] Fix operators and docstrings not being HTML-escaped

Browse Source
This commit is contained in:
Johann Rudloff 2021-05-02 22:54:22 +02:00 committed by G. Allais
parent da51c1c2fe
commit 0490b3de98
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/Doc/HTML.idr
View File

@ -44,7 +44,7 @@ packageInternal _ = pure False
prettyNameRoot : Name -> String prettyNameRoot : Name -> String
prettyNameRoot n = prettyNameRoot n =
let root = nameRoot n in let root = htmlEscape $ nameRoot n in
if isOpName n then "(" ++ root ++ ")" else root if isOpName n then "(" ++ root ++ ")" else root
renderHtml : {auto c : Ref Ctxt Defs} -> renderHtml : {auto c : Ref Ctxt Defs} ->
@ -53,7 +53,7 @@ renderHtml : {auto c : Ref Ctxt Defs} ->
renderHtml STEmpty = pure neutral renderHtml STEmpty = pure neutral
renderHtml (STChar ' ') = pure " " renderHtml (STChar ' ') = pure " "
renderHtml (STChar c) = pure $ cast c renderHtml (STChar c) = pure $ cast c
renderHtml (STText _ text) = pure text renderHtml (STText _ text) = pure $ htmlEscape text
renderHtml (STLine _) = pure "<br>" renderHtml (STLine _) = pure "<br>"
renderHtml (STAnn Declarations rest) = pure $ "<dl class=\"decls\">" <+> !(renderHtml rest) <+> "</dl>" renderHtml (STAnn Declarations rest) = pure $ "<dl class=\"decls\">" <+> !(renderHtml rest) <+> "</dl>"
renderHtml (STAnn (Decl n) rest) = pure $ "<dt id=\"" ++ (htmlEscape $ show n) ++ "\">" <+> !(renderHtml rest) <+> "</dt>" renderHtml (STAnn (Decl n) rest) = pure $ "<dt id=\"" ++ (htmlEscape $ show n) ++ "\">" <+> !(renderHtml rest) <+> "</dt>"