From da51c1c2feb327089441491f1ae2a91649acb119 Mon Sep 17 00:00:00 2001 From: Johann Rudloff Date: Sun, 2 May 2021 22:49:50 +0200 Subject: [PATCH] [ 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). --- src/Idris/Doc/HTML.idr | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Idris/Doc/HTML.idr b/src/Idris/Doc/HTML.idr index 1b5c79509..eaa89810b 100644 --- a/src/Idris/Doc/HTML.idr +++ b/src/Idris/Doc/HTML.idr @@ -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 "
"