on master help sign in
Improve HTML generation for records documentation
commitf5f662c8f8276344844dfbfef346a7bd570c47d1 authorGuglielmo Fachini <guglielmo@fachini.net> dateThu 3 Sep 2015, 23:03 (11 years ago) parent3ec5b5c
1 file changed+10−1
src/Idris/IdrisDoc.hs+10−1
src/Idris/IdrisDoc.hs+10−1
@@ -602,9 +602,12 @@ createOtherDoc ist (RecordDoc n doc ctor projs params) = do
602602 H.span ! class_ "name type"
603603 ! title (toValue $ show n)
604604 $ toHtml $ name $ nsroot n
605− H.span ! class_ "signature" $ nbsp
605+ H.span ! class_ "type" $ do nbsp ; prettyParameters
606606 H.dd $ do
607607 (if nullDocstring doc then Empty else Docstrings.renderHtml doc)
608+ if not $ null params
609+ then H.dl $ forM_ params genParam
610+ else Empty
608611 H.dl ! class_ "decls" $ createFunDoc ist ctor
609612 H.dl ! class_ "decls" $ forM_ projs (createFunDoc ist)
610613 where name (NS n ns) = show (NS (sUN $ name n) ns)
@@ -613,6 +616,12 @@ createOtherDoc ist (RecordDoc n doc ctor projs params) = do
613616 then '(':(n' ++ ")")
614617 else n'
615618
619+ genParam (name, pt, docstring) = do
620+ H.dt $ toHtml $ show (nsroot name)
621+ H.dd $ maybe nbsp Docstrings.renderHtml docstring
622+
623+ prettyParameters = toHtml $ unwords [show $ nsroot n | (n,_,_) <- params]
624+
616625createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do
617626 H.dt ! (A.id $ toValue $ show n) $ do
618627 H.span ! class_ "word" $ do "data"; nbsp