0fe4649 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add a customized display for records documentation

- Update the REPL :doc command output - Update the HTML generation (--mkdoc)

commit0fe4649741b91e35c232611489cad9fba5e7e3f2 authorGuglielmo Fachini <guglielmo@fachini.net> dateWed 2 Sep 2015, 10:31 (11 years ago) parent3f31e4e

2 files changed+62

compare with master

unifiedsplit

src/Idris/Docs.hs+44 src/Idris/IdrisDoc.hs+18

src/Idris/Docs.hs+44

@@ -41,6 +41,10 @@ data Docs' d = FunDoc (FunDoc' d)

4141 [PTerm] -- subclasses

4242 [PTerm] -- superclasses

4343 (Maybe (FunDoc' d)) -- explicit constructor

44+ | RecordDoc Name d -- record docs

45+ (FunDoc' d) -- data constructor docs

46+ [FunDoc' d] -- projection docs

47+ [(Name, PTerm, Maybe d)] -- parameters with type and doc

4448 | NamedInstanceDoc Name (FunDoc' d) -- name is class

4549 | ModDoc [String] -- Module name

4650 d

@@ -209,6 +213,33 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

209213 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

210214 else hsep (punctuate comma (map (prettyName True False params' . fst) params))

211215

216+pprintDocs ist (RecordDoc n doc ctor projs params)

217+ = nest 4 (text "Record" <+> prettyName True (ppopt_impl ppo) [] n <>

218+ if nullDocstring doc

219+ then empty

220+ else line <>

221+ renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

222+ -- Parameters

223+ <$> (if null params

224+ then empty

225+ else line <> nest 4 (text "Parameters:" <$> prettyParameters) <> line)

226+ -- Constructor

227+ <$> nest 4 (text "Constructor:" <$> pprintFDWithoutTotality ist False ctor)

228+ -- Projections

229+ <$> nest 4 (text "Projections:" <$> vsep (map (pprintFDWithoutTotality ist False) projs))

230+ where

231+ ppo = ppOptionIst ist

232+ infixes = idris_infixes ist

233+

234+ pNames = [n | (n,_,_) <- params]

235+ params' = zip pNames (repeat False)

236+

237+ prettyParameters =

238+ if any isJust [d | (_,_,d) <- params]

239+ then vsep (map (\(n,pt,d) -> prettyParam (n,pt) <+> maybe empty (showDoc ist) d) params)

240+ else hsep (punctuate comma (map prettyParam [(n,pt) | (n,pt,_) <- params]))

241+ prettyParam (n,pt) = prettyName True False params' n <+> text ":" <+> pprintPTerm ppo params' [] infixes pt

242+

212243pprintDocs ist (NamedInstanceDoc _cls doc)

213244 = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist True doc)

214245

@@ -234,6 +265,8 @@ getDocs n w

234265 = do i <- getIState

235266 docs <- if | Just ci <- lookupCtxtExact n (idris_classes i)

236267 -> docClass n ci

268+ | Just ri <- lookupCtxtExact n (idris_records i)

269+ -> docRecord n ri

237270 | Just ti <- lookupCtxtExact n (idris_datatypes i)

238271 -> docData n ti

239272 | Just class_ <- classNameForInst i n

@@ -296,6 +329,17 @@ docClass n ci

296329 isSubclass _

297330 = False

298331

332+docRecord :: Name -> RecordInfo -> Idris Docs

333+docRecord n ri

334+ = do i <- getIState

335+ let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

336+ docstr = maybe emptyDocstring fst docStrings

337+ params = map (\(pn,pt) -> (pn, pt, docStrings >>= (lookup pn . snd)))

338+ (record_parameters ri)

339+ pdocs <- mapM docFun (record_projections ri)

340+ ctorDocs <- docFun $ record_constructor ri

341+ return $ RecordDoc n docstr ctorDocs pdocs params

342+

299343docFun :: Name -> Idris FunDoc

300344docFun n

301345 = do i <- getIState

src/Idris/IdrisDoc.hs+18

@@ -221,6 +221,7 @@ referredNss (n, Just d, _) =

221221 where getFunDocs (FunDoc f) = [f]

222222 getFunDocs (DataDoc f fs) = f:fs

223223 getFunDocs (ClassDoc _ _ fs _ _ _ _ _) = fs

224+ getFunDocs (RecordDoc _ _ f fs _) = f:fs

224225 getFunDocs (NamedInstanceDoc _ fd) = [fd]

225226 getFunDocs (ModDoc _ _) = []

226227 types (FD _ _ args t _) = t:(map second args)

@@ -595,6 +596,23 @@ createOtherDoc ist (ClassDoc n docstring fds _ _ _ _ c) = do

595596 then '(':(n' ++ ")")

596597 else n'

597598

599+createOtherDoc ist (RecordDoc n doc ctor projs params) = do

600+ H.dt ! (A.id $ toValue $ show n) $ do

601+ H.span ! class_ "word" $ do "record"; nbsp

602+ H.span ! class_ "name type"

603+ ! title (toValue $ show n)

604+ $ toHtml $ name $ nsroot n

605+ H.span ! class_ "signature" $ nbsp

606+ H.dd $ do

607+ (if nullDocstring doc then Empty else Docstrings.renderHtml doc)

608+ H.dl ! class_ "decls" $ createFunDoc ist ctor

609+ H.dl ! class_ "decls" $ forM_ projs (createFunDoc ist)

610+ where name (NS n ns) = show (NS (sUN $ name n) ns)

611+ name n = let n' = show n

612+ in if (head n') `elem` opChars

613+ then '(':(n' ++ ")")

614+ else n'

615+

598616createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do

599617 H.dt ! (A.id $ toValue $ show n) $ do

600618 H.span ! class_ "word" $ do "data"; nbsp