git.iko.soy/Idris-dev
on master help sign in
Use the pretty-printer to show :doc
791bd36David Raymond Christiansen
src/Idris/Docs.hs+44−45
compare with master
unifiedsplit
@@ -6,63 +6,62 @@ import Idris.Delaborate
6import Idris.Core.TT
6import Idris.Core.TT
7import Idris.Core.Evaluate
7import Idris.Core.Evaluate
8
8
9+import Util.Pretty
10+
9import Data.Maybe
11import Data.Maybe
10import Data.List
12import Data.List
11
13
12-- TODO: Only include names with public/abstract accessibility
14-- TODO: Only include names with public/abstract accessibility
13
15
14−data FunDoc = Doc Name String
16+data FunDoc = FD Name String
15− [(Name, PArg)] -- args
17+ [(Name, PArg)] -- args
16− PTerm -- function type
18+ PTerm -- function type
17− (Maybe Fixity)
19+ (Maybe Fixity)
18−
20+
19−data Doc = FunDoc FunDoc
21+data Docs = FunDoc FunDoc
20− | DataDoc FunDoc -- type constructor docs
22+ | DataDoc FunDoc -- type constructor docs
21− [FunDoc] -- data constructor docs
23+ [FunDoc] -- data constructor docs
22− | ClassDoc Name String -- class docs
24+ | ClassDoc Name String -- class docs
23− [FunDoc] -- method docs
25+ [FunDoc] -- method docs
24−
26+
25−showDoc "" = ""
27+showDoc "" = empty
26−showDoc x = " -- " ++ x
28+showDoc x = text " -- " <> text x
27−
29+
28−instance Show FunDoc where
30+pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
29− show (Doc n doc args ty f)
31+pprintFD imp (FD n doc args ty f)
30− = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++ "\n" ++
32+ = prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>
31− maybe "" (\f -> show f ++ "\n\n") f ++
33+ maybe empty (\f -> text (show f) <> line) f <>
32− let argshow = mapMaybe showArg args in
34+ let argshow = mapMaybe showArg args in
33− if not (null argshow)
35+ if not (null argshow)
34− then "Arguments:\n\t" ++ showSep "\t" argshow
36+ then nest 4 $ text "Arguments:" <$> vsep argshow
35− else ""
37+ else empty
36
38
37 where showArg (n, arg@(PExp _ _ _ _))
39 where showArg (n, arg@(PExp _ _ _ _))
38− = Just $ showName n ++ show (getTm arg) ++
40+ = Just $ bindingOf n False <> prettyImp imp (getTm arg) <>
39− showDoc (pargdoc arg) ++ "\n"
41+ showDoc (pargdoc arg) <> line
40 showArg (n, arg@(PConstraint _ _ _ _))
42 showArg (n, arg@(PConstraint _ _ _ _))
41− = Just $ "Class constraint " ++
43+ = Just $ text "Class constraint" <+>
42− show (getTm arg) ++ showDoc (pargdoc arg)
44+ prettyImp imp (getTm arg) <> showDoc (pargdoc arg) <> line
43− ++ "\n"
44 showArg (n, arg@(PImp _ _ _ _ _ doc))
45 showArg (n, arg@(PImp _ _ _ _ _ doc))
45 | not (null doc)
46 | not (null doc)
46− = Just $ "(implicit) " ++
47+ = Just $ text "(implicit)" <+>
47− show n ++ " : " ++ show (getTm arg)
48+ bindingOf n True <+> colon <+> prettyImp imp (getTm arg)
48− ++ showDoc (pargdoc arg) ++ "\n"
49+ <> showDoc (pargdoc arg) <> line
49 showArg (n, _) = Nothing
50 showArg (n, _) = Nothing
50
51
51− showName (MN _ _) = ""
52− showName x = show x ++ " : "
53
52
54−instance Show Doc where
55
53
56− show (FunDoc d) = show d
54+pprintDocs imp (FunDoc d) = pprintFD imp d
57− show (DataDoc t args) = "Data type " ++ show t ++
55+pprintDocs imp (DataDoc t args)
58− "\nConstructors:\n\n" ++
56+ = text "Data type" <+> pprintFD imp t <$>
59− showSep "\n" (map show args)
57+ nest 4 (text "Constructors:" <> line <>
58+ vsep (map (pprintFD imp) args))
60− show (ClassDoc n doc meths)
59+pprintDocs imp (ClassDoc n doc meths)
61− = "Type class " ++ show n ++ -- parameters?
60+ = text "Type class" <+> prettyName imp [] n <$> -- parameters?
62− "\nMethods:\n\n" ++
61+ nest 4 (text "Methods:" <$>
63− showSep "\n" (map show meths)
62+ vsep (map (pprintFD imp) meths))
64
63
65−getDocs :: Name -> Idris Doc
64+getDocs :: Name -> Idris Docs
66getDocs n
65getDocs n
67 = do i <- getIState
66 = do i <- getIState
68 case lookupCtxt n (idris_classes i) of
67 case lookupCtxt n (idris_classes i) of
@@ -72,13 +71,13 @@ getDocs n
72 _ -> do fd <- docFun n
71 _ -> do fd <- docFun n
73 return (FunDoc fd)
72 return (FunDoc fd)
74
73
75−docData :: Name -> TypeInfo -> Idris Doc
74+docData :: Name -> TypeInfo -> Idris Docs
76docData n ti
75docData n ti
77 = do tdoc <- docFun n
76 = do tdoc <- docFun n
78 cdocs <- mapM docFun (con_names ti)
77 cdocs <- mapM docFun (con_names ti)
79 return (DataDoc tdoc cdocs)
78 return (DataDoc tdoc cdocs)
80
79
81−docClass :: Name -> ClassInfo -> Idris Doc
80+docClass :: Name -> ClassInfo -> Idris Docs
82docClass n ci
81docClass n ci
83 = do i <- getIState
82 = do i <- getIState
84 let docstr = case lookupCtxt n (idris_docstrings i) of
83 let docstr = case lookupCtxt n (idris_docstrings i) of
@@ -105,7 +104,7 @@ docFun n
105 [] -> Nothing
104 [] -> Nothing
106 (Fix x _:_) -> Just x
105 (Fix x _:_) -> Just x
107
106
108− return (Doc n docstr args (delab i ty) f)
107+ return (FD n docstr args (delab i ty) f)
109 where funName :: Name -> String
108 where funName :: Name -> String
110 funName (UN n) = str n
109 funName (UN n) = str n
111 funName (NS n _) = funName n
110 funName (NS n _) = funName n
src/Idris/REPL.hs+8−8
@@ -521,14 +521,14 @@ process h fn (Check t)
521 (prettyImp imp (delab ist ty))
521 (prettyImp imp (delab ist ty))
522
522
523process h fn (DocStr n)
523process h fn (DocStr n)
524− = do i <- getIState
524+ = do i <- getIState
525+ let imp = opt_showimp (idris_options i)
525− case lookupCtxtName n (idris_docstrings i) of
526+ case lookupCtxtName n (idris_docstrings i) of
526− [] -> iPrintError $ "No documentation for " ++ show n
527+ [] -> iPrintError $ "No documentation for " ++ show n
527− ns -> do mapM_ showDoc ns
528+ ns -> do toShow <- mapM (showDoc imp) ns
528− iPrintResult ""
529+ ihRenderResult h (vsep toShow)
529− where showDoc (n, d)
530+ where showDoc imp (n, d) = do doc <- getDocs n
530− = do doc <- getDocs n
531+ return $ pprintDocs imp doc
531− iputStrLn $ show doc
532process h fn Universes
532process h fn Universes
533 = do i <- getIState
533 = do i <- getIState
534 let cs = idris_constraints i
534 let cs = idris_constraints i