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

[ docs ] Remove unnecessary newlines in HTML declaration lists

Browse Source 
As a relict of the REPL output, several `<br>` tags where introduced,
where they are not needed or even permitted. This led to some spacing
issues (sometimes the docstring was closer to the next term than to the
one above that it actually described).

To counter the removed forced newlines, some extra margin is added below
each declaration.

As a side-effect, this also makes the W3 "Nu Html Checker" happy.
This commit is contained in:
Johann Rudloff 2021-05-05 19:55:17 +02:00 committed by G. Allais
parent 0ab5fe2535
commit 190932fd01
2 changed files with 14 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -80,12 +80,23 @@ renderHtml (STAnn ann rest) = do
pure $ "<!-- ann ignored START -->" ++ resthtml ++ "<!-- ann END -->"
renderHtml (STConcat docs) = pure $ fastConcat !(traverse renderHtml docs)
removeNewlinesFromDeclarations : SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
removeNewlinesFromDeclarations = go False
where
go : Bool -> SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
go False l@(STLine i) = l
go True l@(STLine i) = STEmpty
go ignoring (STConcat docs) = STConcat $ map (go ignoring) docs
go _ (STAnn Declarations rest) = STAnn Declarations $ go True rest
go _ (STAnn ann rest) = STAnn ann $ go False rest
go _ doc = doc
docDocToHtml : {auto c : Ref Ctxt Defs} ->
Doc IdrisDocAnn ->
Core String
docDocToHtml doc =
let dt = SimpleDocTree.fromStream $ layoutUnbounded doc in
renderHtml dt
renderHtml $ removeNewlinesFromDeclarations dt
htmlPreamble : String -> String -> String -> String
htmlPreamble title root class = "<!DOCTYPE html><html lang=\"en\"><head><meta charset=\"utf-8\">"

4
support/docs/styles.css
View File

@ -94,7 +94,7 @@ p {
}
.decls {
margin-top: 15px;
margin-top: 5px;
}
.decls > dt {
@ -111,7 +111,7 @@ p {
}
.decls > dd {
margin: 10px 0 10px 20px;
margin: 10px 0 20px 20px;
font-family: Arial, sans-serif;
font-size: 10pt;
}