09d107a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change namespace display in :t and :doc

:t on names only shows the namespace if necessary for disambiguation or if showimplicits is on (which is consistent with other :t behaviour) :doc now *always* shows namespaces (previously, it never showed them)

commit09d107aa286144c3be2fe723ba2492923e866ff2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 1 Jul 2015, 23:12 (11 years ago) parentd23c653

2 files changed+4−3

compare with master

unifiedsplit

src/Idris/Docs.hs+1−1 src/Idris/Output.hs+3−2

src/Idris/Docs.hs+1−1

@@ -55,7 +55,7 @@ showDoc ist d

5555

5656pprintFD :: IState -> Bool -> FunDoc -> Doc OutputAnnotation

5757pprintFD ist totalityFlag (FD n doc args ty f)

58− = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>

58+ = nest 4 (prettyName True True [] n <+> colon <+>

5959 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

6060 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

6161 -- show doc

src/Idris/Output.hs+3−2

@@ -87,9 +87,10 @@ iPrintFunTypes bnd n overloads = do ist <- getIState

8787 let infixes = idris_infixes ist

8888 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

8989 iRenderResult output

90− where fullName n = prettyName True True bnd n

90+ where fullName ppo n | length overloads > 1 = prettyName True True bnd n

91+ | otherwise = prettyName True (ppopt_impl ppo) bnd n

9192 ppOverload ppo infixes n tm =

92− fullName n <+> colon <+> align tm

93+ fullName ppo n <+> colon <+> align tm

9394

9495iRenderOutput :: Doc OutputAnnotation -> Idris ()

9596iRenderOutput doc =