497caf0 · Idris-dev · git.iko.soy

src/Idris/Output.hs+2−2

@@ -68,7 +68,7 @@ iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

68iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)

69

70-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

71−iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

71+iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()

72iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n

73iPrintFunTypes bnd n overloads = do ist <- getIState

74 let ppo = ppOptionIst ist

@@ -77,7 +77,7 @@ iPrintFunTypes bnd n overloads = do ist <- getIState

77 iRenderResult output

78 where fullName n = prettyName True True bnd n

79 ppOverload ppo infixes n tm =

80− fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

80+ fullName n <+> colon <+> align tm

81

82iRenderOutput :: Doc OutputAnnotation -> Idris ()

83iRenderOutput doc =

src/Idris/Prover.hs+1−1

@@ -274,7 +274,7 @@ ploop fn d prompt prf e h

274 -- make it easier to see how to prove with them.

275 let action = case lookupNames n ctxt' of

276 [] -> iPrintError $ "No such variable " ++ show n

277− ts -> iPrintFunTypes bnd n (map (\n -> (n, delabTy ist' n)) ts)

277+ ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)

278 putIState ist

279 return (False, e, False, prf, Right action))

280 (\err -> do putIState ist ; ierror err)

src/Idris/REPL.hs+1−1

@@ -819,7 +819,7 @@ process fn (Check (PRef _ n))

819 case lookup t (idris_metavars ist) of

820 Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $

821 showMetavarInfo ppo ist n i

822− Nothing -> iPrintFunTypes [] n (map (\n -> (n, delabTy ist n)) ts)

822+ Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

823 [] -> iPrintError $ "No such variable " ++ show n

824 where

825 showMetavarInfo ppo ist n i