idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-15 14:23:32 +03:00
Code Issues Projects Releases Wiki Activity

[ docs ] Fix record fields wrapped in parentheses in HTML doc

Browse Source 
The (implicitly added) "."-prefix when calling `isOpName` with an RF-name
leads to `isOpName` always returning true (which is correct in most
cases, where the RF is displayed as such). In case of the docs however,
we only show the name root and thus should check the "real" name of the
field (without the added dot in the beginning).
This commit is contained in:
Johann Rudloff 2021-06-30 20:01:57 +02:00 committed by G. Allais
parent f2f83bd531
commit af9f72466f
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -46,8 +46,11 @@ packageInternal _ = pure False
prettyNameRoot : Name -> String
prettyNameRoot n =
let root = htmlEscape $ nameRoot n in
if isOpName n then "(" ++ root ++ ")" else root
let root = nameRoot n in
-- We need to take the root first and then re-wrap in a UN for the op check
-- to avoid false positives for record fields (RF) names (which get an
-- implicit "."-prefix).
htmlEscape (if isOpName (UN root) then "(" ++ root ++ ")" else root)
renderHtml : {auto c : Ref Ctxt Defs} ->
SimpleDocTree IdrisDocAnn ->