mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 19:13:02 +03:00
[ docs ] Fix #1367: Missing spaces in type signatures in WebKit-based browsers
WebKit seems to throw away any sequence of spaces between inline tags. All affected places I found could be fixed by replacing single space characters with the character U+2002 ("EN Space"), which means almost the same thing as "normal space" (i.e. it breaks/wraps text and has approximately the same width) but is not discarded by WebKit when parsing the document. If this should come up in a different place, a more thorough solution might be needed (e.g. modifying `htmlEscape` to replace all spaces).
This commit is contained in:
parent
182a3caa3e
commit
da51c1c2fe
@ -51,6 +51,7 @@ renderHtml : {auto c : Ref Ctxt Defs} ->
|
||||
SimpleDocTree IdrisDocAnn ->
|
||||
Core String
|
||||
renderHtml STEmpty = pure neutral
|
||||
renderHtml (STChar ' ') = pure " "
|
||||
renderHtml (STChar c) = pure $ cast c
|
||||
renderHtml (STText _ text) = pure text
|
||||
renderHtml (STLine _) = pure "<br>"
|
||||
|
Loading…
Reference in New Issue
Block a user