Skip to content

Commit

Permalink
[ mkdoc ] Wrap declaration part in <code> tag
Browse files Browse the repository at this point in the history
  • Loading branch information
gemmaro authored and gallais committed Nov 18, 2021
1 parent 489e8c7 commit c7df419
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Idris/Doc/HTML.idr
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ renderHtml (STText _ text) = pure $ htmlEscape text
renderHtml (STLine _) = pure "<br>"
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) ++ "\"><code>" <+> !(renderHtml rest) <+> "</code></dt>"
renderHtml (STAnn DocStringBody rest)
= pure $ "<dd>" <+> !(renderHtml rest) <+> "</dd>"
renderHtml (STAnn UserDocString rest)
Expand Down

0 comments on commit c7df419

Please sign in to comment.