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

git.iko.soy/Idris-dev

Make output from :t name annotate with terms

This lets IDEs do things like normalise the output from :t. Previously, it worked for :t of a term, but not :t of a name.

commit497caf077bfd8ba978c8b15f5cf71b7aa65f87eb authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 24 Sep 2014, 08:50 (12 years ago) parent7572017

3 files changed+4−4

compare with master

unifiedsplit

src/Idris/Output.hs+2−2 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+1−1

src/Idris/Output.hs+2−2

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

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

6969

7070-- | 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 ()

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

7373iPrintFunTypes bnd n overloads = do ist <- getIState

7474 let ppo = ppOptionIst ist

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

7777 iRenderResult output

7878 where fullName n = prettyName True True bnd n

7979 ppOverload ppo infixes n tm =

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

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

8181

8282iRenderOutput :: Doc OutputAnnotation -> Idris ()

8383iRenderOutput doc =

src/Idris/Prover.hs+1−1

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

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

275275 let action = case lookupNames n ctxt' of

276276 [] -> 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)

278278 putIState ist

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

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

src/Idris/REPL.hs+1−1

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

819819 case lookup t (idris_metavars ist) of

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

821821 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)

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

824824 where

825825 showMetavarInfo ppo ist n i