git.iko.soy/Idris-dev
on master help sign in
Show visibility in doc comments.
36bcf4bJan de Muijnck-Hughes
src/Idris/Core/Evaluate.hs+7
compare with master
unifiedsplit
@@ -24,6 +24,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
24 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
24 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
25 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
25 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
26 mapDefCtxt, tcReducible,
26 mapDefCtxt, tcReducible,
27+ lookupTotalAccessibility,
27 lookupTotal, lookupTotalExact, lookupInjectiveExact,
28 lookupTotal, lookupTotalExact, lookupInjectiveExact,
28 lookupRigCount, lookupRigCountExact,
29 lookupRigCount, lookupRigCountExact,
29 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
30 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
@@ -1167,6 +1168,12 @@ lookupDefAcc n mkpublic ctxt
1167 where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
1168 where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
1168 then (d, Public) else (d, a)
1169 then (d, Public) else (d, a)
1169
1170
1171+lookupTotalAccessibility :: Name -> Context -> [(Totality,Accessibility)]
1172+lookupTotalAccessibility n ctxt = fmap unpack $ lookupCtxt n (definitions ctxt)
1173+
1174+ where
1175+ unpack ((_,_,_,a,t,_)) = (t,a)
1176+
1170lookupDefAccExact :: Name -> Bool -> Context ->
1177lookupDefAccExact :: Name -> Bool -> Context ->
1171 Maybe (Def, Accessibility)
1178 Maybe (Def, Accessibility)
1172lookupDefAccExact n mkpublic ctxt
1179lookupDefAccExact n mkpublic ctxt
src/Idris/Docs.hs+11−6
@@ -94,11 +94,9 @@ pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
94 (if not (null argshow)
94 (if not (null argshow)
95 then nest 4 $ text "Arguments:" <$> vsep argshow
95 then nest 4 $ text "Arguments:" <$> vsep argshow
96 else empty)
96 else empty)
97− -- show totality status
97+ -- show totality and visibility status
98− <> let totality = getTotality in
98+ <> showTotalVisibility
99− (if totalityFlag && not (null totality)
99+ )
100− then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
101− else empty))
102
100
103 where
101 where
104 ppo = ppOptionIst ist
102 ppo = ppOptionIst ist
@@ -135,7 +133,14 @@ pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
135 showArgs args ((n, True):bnd)
133 showArgs args ((n, True):bnd)
136 showArgs [] _ = [] -- end of arguments
134 showArgs [] _ = [] -- end of arguments
137
135
138− getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
136+ showTotalVisibility =
137+ case lookupTotalAccessibility n (tt_ctxt ist) of
138+ [] -> empty
139+ xs -> line <> vsep (map (doShowTotalVisibility) xs)
140+
141+ doShowTotalVisibility (t,v) = if totalityFlag
142+ then text "The function is:" <+> ((text . show) t) <+> (text "&") <+> ((text . show) v)
143+ else text "The function is:" <+> ((text . show) v)
139
144
140pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
145pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
141pprintFDWithTotality ist = pprintFD ist True
146pprintFDWithTotality ist = pprintFD ist True