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

git.iko.soy/Idris-dev

on master help sign in

Add a customized display for records documentation

0fe4649Guglielmo Fachini11 years ago

src/Idris/Docs.hs+44

compare with master

unifiedsplit

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

41 [PTerm] -- subclasses

42 [PTerm] -- superclasses

43 (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

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

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

45 | ModDoc [String] -- Module name

49 | ModDoc [String] -- Module name

46 d

50 d

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

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

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

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

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

211

215

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+

212pprintDocs ist (NamedInstanceDoc _cls doc)

243pprintDocs ist (NamedInstanceDoc _cls doc)

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

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

214

245

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

234 = do i <- getIState

265 = do i <- getIState

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

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

236 -> docClass n ci

267 -> docClass n ci

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

269+ -> docRecord n ri

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

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

238 -> docData n ti

271 -> docData n ti

239 | Just class_ <- classNameForInst i n

272 | Just class_ <- classNameForInst i n

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

296 isSubclass _

329 isSubclass _

297 = False

330 = False

298

331

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+

299docFun :: Name -> Idris FunDoc

343docFun :: Name -> Idris FunDoc

300docFun n

344docFun n

301 = do i <- getIState

345 = do i <- getIState

src/Idris/IdrisDoc.hs+18

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

221 where getFunDocs (FunDoc f) = [f]

222 getFunDocs (DataDoc f fs) = f:fs

223 getFunDocs (ClassDoc _ _ fs _ _ _ _ _) = fs

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

224 getFunDocs (NamedInstanceDoc _ fd) = [fd]

225 getFunDocs (NamedInstanceDoc _ fd) = [fd]

225 getFunDocs (ModDoc _ _) = []

226 getFunDocs (ModDoc _ _) = []

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

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

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

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

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

596 else n'

597 else n'

597

598

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+

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

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

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

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

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

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