8cc769b · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+12−3

compare with master

unifiedsplit

@@ -1342,9 +1342,18 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1342 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1343 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1344 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1345− prettySe p bnd (PEq _ _ _ l r) =

1345+ prettySe p bnd (PEq _ lt rt l r)

1346+ | ppopt_impl ppo =

1347+ bracket p 1 $

1348+ enclose lparen rparen eq <+>

1349+ align (group (vsep (map (prettyArgS bnd)

1350+ [PImp 0 False [] (sUN "A") lt,

1351+ PImp 0 False [] (sUN "B") rt,

1352+ PExp 0 [] (sUN "x") l,

1353+ PExp 0 [] (sUN "y") r])))

1354+ | otherwise =

1346− bracket p 2 . align . group $

1355+ bracket p 2 . align . group $

1347− prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1356+ prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1348 where eq = annName eqTy (text "=")

1357 where eq = annName eqTy (text "=")

1349 prettySe p bnd (PRewrite _ l r _) =

1358 prettySe p bnd (PRewrite _ l r _) =

1350 bracket p 2 $

1359 bracket p 2 $

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