git.iko.soy/Idris-dev
on master help sign in
added fixity of operators to :doc output
39e0fbaraichoo
src/Idris/Docs.hs+16−5
compare with master
unifiedsplit
@@ -1,17 +1,20 @@
1module Idris.Docs where
1module Idris.Docs where
2
2
3import Idris.AbsSyntax
3import Idris.AbsSyntax
4+import Idris.AbsSyntaxTree
4import Idris.Delaborate
5import Idris.Delaborate
5import Core.TT
6import Core.TT
6import Core.Evaluate
7import Core.Evaluate
7
8
8import Data.Maybe
9import Data.Maybe
10+import Data.List
9
11
10-- TODO: Only include names with public/abstract accessibility
12-- TODO: Only include names with public/abstract accessibility
11
13
12data FunDoc = Doc Name String
14data FunDoc = Doc Name String
13 [(Name, PArg)] -- args
15 [(Name, PArg)] -- args
14 PTerm -- function type
16 PTerm -- function type
17+ (Maybe Fixity)
15
18
16data Doc = FunDoc FunDoc
19data Doc = FunDoc FunDoc
17 | DataDoc FunDoc -- type constructor docs
20 | DataDoc FunDoc -- type constructor docs
@@ -23,12 +26,14 @@ showDoc "" = ""
23showDoc x = " -- " ++ x
26showDoc x = " -- " ++ x
24
27
25instance Show FunDoc where
28instance Show FunDoc where
26− show (Doc n doc args ty)
29+ show (Doc n doc args ty f)
27 = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++ "\n" ++
30 = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++ "\n" ++
31+ maybe "" (\f -> show f ++ "\n\n") f ++
28 let argshow = mapMaybe showArg args in
32 let argshow = mapMaybe showArg args in
29− if (not (null argshow)) then "Arguments:\n\t" ++
33+ if not (null argshow)
30− showSep "\t" argshow
34+ then "Arguments:\n\t" ++ showSep "\t" argshow
31− else ""
35+ else ""
36+
32 where showArg (n, arg@(PExp _ _ _ _))
37 where showArg (n, arg@(PExp _ _ _ _))
33 = Just $ showName n ++ show (getTm arg) ++
38 = Just $ showName n ++ show (getTm arg) ++
34 showDoc (pargdoc arg) ++ "\n"
39 showDoc (pargdoc arg) ++ "\n"
@@ -94,6 +99,12 @@ docFun n
94 let args = case lookupCtxt Nothing n (idris_implicits i) of
99 let args = case lookupCtxt Nothing n (idris_implicits i) of
95 [args] -> zip argnames args
100 [args] -> zip argnames args
96 _ -> []
101 _ -> []
102+ let infixes = idris_infixes i
103+ let fixdecls = filter (\(Fix _ x) -> x `isSuffixOf` (show n)) infixes
104+ let f = case fixdecls of
105+ [] -> Nothing
106+ (Fix x _:_) -> Just x
107+
97− return (Doc n docstr args (delab i ty))
108+ return (Doc n docstr args (delab i ty) f)
98
109
99
110