044ba30 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #827 from david-christiansen/semantic-pprint

044ba30Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+27−4

compare with master

unifiedsplit

@@ -407,6 +407,21 @@ getUndefined :: Idris [Name]

407getUndefined = do i <- getIState

408 return (map fst (idris_metavars i) \\ primDefs)

409

410+getWidth :: Idris ConsoleWidth

411+getWidth = fmap idris_consolewidth getIState

412+

413+setWidth :: ConsoleWidth -> Idris ()

414+setWidth w = do ist <- getIState

415+ put ist { idris_consolewidth = w }

416+

417+iRender :: Doc a -> Idris (SimpleDoc a)

418+iRender d = do w <- getWidth

419+ return $ case w of

420+ InfinitelyWide -> renderPretty 1.0 1000000000 d

421+ ColsWide n -> if n < 1

422+ then renderPretty 1.0 1000000000 d

423+ else renderPretty 0.5 n d

424+

410ihPrintResult :: Handle -> String -> Idris ()

425ihPrintResult :: Handle -> String -> Idris ()

411ihPrintResult h s = do i <- getIState

426ihPrintResult h s = do i <- getIState

412 case idris_outputmode i of

427 case idris_outputmode i of

@@ -420,15 +435,17 @@ ihPrintResult h s = do i <- getIState

420-- | Write a pretty-printed term to the console with semantic coloring

435-- | Write a pretty-printed term to the console with semantic coloring

421consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

436consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

422consoleDisplayAnnotated h output = do ist <- getIState

437consoleDisplayAnnotated h output = do ist <- getIState

438+ rendered <- iRender $ output

423 runIO . hPutStrLn h .

439 runIO . hPutStrLn h .

424− displayDecorated (consoleDecorate ist) .

440+ displayDecorated (consoleDecorate ist) $

425− renderCompact $ output

441+ rendered

442+

426

443

427-- | Write pretty-printed output to IDESlave with semantic annotations

444-- | Write pretty-printed output to IDESlave with semantic annotations

428ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

445ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

429ideSlaveReturnAnnotated n h out = do ist <- getIState

446ideSlaveReturnAnnotated n h out = do ist <- getIState

430 let (str, spans) = displaySpans .

447 let (str, spans) = displaySpans .

431− renderCompact .

448+ renderPretty 0.8 80 .

432 fmap (fancifyAnnots ist) $

449 fmap (fancifyAnnots ist) $

433 out

450 out

434 good = [SymbolAtom "ok", toSExp str, toSExp spans]

451 good = [SymbolAtom "ok", toSExp str, toSExp spans]

@@ -451,7 +468,13 @@ ihPrintFunTypes h n overloads = do imp <- impShow

451 RawOutput -> consoleDisplayAnnotated h output

468 RawOutput -> consoleDisplayAnnotated h output

452 IdeSlave n -> ideSlaveReturnAnnotated n h output

469 IdeSlave n -> ideSlaveReturnAnnotated n h output

453 where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)

470 where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)

454− ppOverload imp n tm = fullName n <+> colon <+> prettyImp imp tm

471+ ppOverload imp n tm = fullName n <+> colon <+> align (prettyImp imp tm)

472+

473+ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

474+ihRenderResult h d = do ist <- getIState

475+ case idris_outputmode ist of

476+ RawOutput -> consoleDisplayAnnotated h d

477+ IdeSlave n -> ideSlaveReturnAnnotated n h d

455

478

456fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

479fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

457fancifyAnnots ist annot@(AnnName n _ _) =

480fancifyAnnots ist annot@(AnnName n _ _) =

src/Idris/AbsSyntaxTree.hs+46−78

@@ -22,7 +22,7 @@ import System.IO

22import Control.Monad.Trans.State.Strict

23import Control.Monad.Trans.Error

25−import Data.List

25+import Data.List hiding (group)

26import Data.Char

27import qualified Data.Map as M

28import qualified Data.Text as T

@@ -83,6 +83,10 @@ data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord

83-- | The output mode in use

84data OutputMode = RawOutput | IdeSlave Integer deriving Show

86+-- | How wide is the console?

87+data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

88+ | ColsWide Int -- ^ Must be positive

89+

86-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

90-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

87-- without typechecking).

91-- without typechecking).

88-- This will include all the functions and data declarations, plus fixity declarations

92-- This will include all the functions and data declarations, plus fixity declarations

@@ -144,8 +148,8 @@ data IState = IState {

144 idris_errorhandlers :: [Name], -- ^ Global error handlers

148 idris_errorhandlers :: [Name], -- ^ Global error handlers

145 idris_nameIdx :: (Int, Ctxt (Int, Name)),

149 idris_nameIdx :: (Int, Ctxt (Int, Name)),

146 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

150 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

147− module_aliases :: M.Map [T.Text] [T.Text]

151+ module_aliases :: M.Map [T.Text] [T.Text],

148−

152+ idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?

149 }

153 }

150

154

151data SizeChange = Smaller | Same | Bigger | Unknown

155data SizeChange = Smaller | Same | Bigger | Unknown

@@ -215,6 +219,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

215 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

219 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

216 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

220 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

217 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

221 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

222+ (ColsWide 80)

218

223

219-- | The monad for the main REPL - reading and processing files and updating

224-- | The monad for the main REPL - reading and processing files and updating

220-- global state (hence the IO inner monad).

225-- global state (hence the IO inner monad).

@@ -691,7 +696,6 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

691deriving instance Binary PTactic'

696deriving instance Binary PTactic'

692deriving instance NFData PTactic'

697deriving instance NFData PTactic'

693!-}

698!-}

694−

695instance Sized a => Sized (PTactic' a) where

699instance Sized a => Sized (PTactic' a) where

696 size (Intro nms) = 1 + size nms

700 size (Intro nms) = 1 + size nms

697 size Intros = 1

701 size Intros = 1

@@ -1010,17 +1014,20 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

1010

1014

1011-- Pretty-printing declarations and terms

1015-- Pretty-printing declarations and terms

1012

1016

1017+-- These "show" instances render to an absurdly wide screen because inserted line breaks

1018+-- could interfere with interactive editing, which calls "show".

1019+

1013instance Show PTerm where

1020instance Show PTerm where

1014− showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm

1021+ showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm

1015

1022

1016instance Show PDecl where

1023instance Show PDecl where

1017− showsPrec _ d = (displayS . renderCompact . showDeclImp False) d

1024+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d

1018

1025

1019instance Show PClause where

1026instance Show PClause where

1020− showsPrec _ c = (displayS . renderCompact . showCImp True) c

1027+ showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c

1021

1028

1022instance Show PData where

1029instance Show PData where

1023− showsPrec _ d = (displayS . renderCompact . showDImp False) d

1030+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d

1024

1031

1025instance Pretty PTerm OutputAnnotation where

1032instance Pretty PTerm OutputAnnotation where

1026 pretty = prettyImp False

1033 pretty = prettyImp False

@@ -1060,9 +1067,6 @@ pprintPTerm impl bnd = prettySe 10 bnd

1060 where

1067 where

1061 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1068 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1062 prettySe p bnd (PQuote r) =

1069 prettySe p bnd (PQuote r) =

1063− if size r > breakingSize then

1064− text "![" <> line <> pretty r <> text "]"

1065− else

1066 text "![" <> pretty r <> text "]"

1070 text "![" <> pretty r <> text "]"

1067 prettySe p bnd (PPatvar fc n) = pretty n

1071 prettySe p bnd (PPatvar fc n) = pretty n

1068 prettySe p bnd e

1072 prettySe p bnd e

@@ -1070,35 +1074,23 @@ pprintPTerm impl bnd = prettySe 10 bnd

1070 | Just n <- snat p e = annotate AnnConstData (text (show n))

1074 | Just n <- snat p e = annotate AnnConstData (text (show n))

1071 prettySe p bnd (PRef fc n) = prettyName impl bnd n

1075 prettySe p bnd (PRef fc n) = prettyName impl bnd n

1072 prettySe p bnd (PLam n ty sc) =

1076 prettySe p bnd (PLam n ty sc) =

1073− bracket p 2 $

1077+ bracket p 2 . group . hang 2 $

1074− if size sc > breakingSize then

1078+ text "\\" <> bindingOf n False <+> text "=>" <$>

1075− text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc

1076− else

1077− text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc

1079+ prettySe 10 ((n, False):bnd) sc

1078 prettySe p bnd (PLet n ty v sc) =

1080 prettySe p bnd (PLet n ty v sc) =

1079 bracket p 2 $

1081 bracket p 2 $

1080− if size sc > breakingSize then

1081− text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>

1082+ text "let" <+> bindingOf n False <+> text "=" </>

1082− nest nestingSize (prettySe 10 ((n, False):bnd) sc)

1083− else

1084− text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>

1083+ prettySe 10 bnd v <+> text "in" </>

1085− prettySe 10 ((n, False):bnd) sc

1084+ prettySe 10 ((n, False):bnd) sc

1086 prettySe p bnd (PPi (Exp l s _ _) n ty sc)

1085 prettySe p bnd (PPi (Exp l s _ _) n ty sc)

1087 | n `elem` allNamesIn sc || impl =

1086 | n `elem` allNamesIn sc || impl =

1088 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1087 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1089− bracket p 2 $

1088+ bracket p 2 . group $

1090− if size sc > breakingSize then

1089+ enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1091− enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1092− st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc

1093− else

1094− enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1095− st <> text "->" <+> prettySe 10 ((n, False):bnd) sc

1090+ st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1096 | otherwise =

1091 | otherwise =

1097− bracket p 2 $

1092+ bracket p 2 . group $

1098− if size sc > breakingSize then

1099− prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc

1093+ group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1100− else

1101− prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc

1102 where

1094 where

1103 st =

1095 st =

1104 case s of

1096 case s of

@@ -1108,12 +1100,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

1108 | impl =

1100 | impl =

1109 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1101 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1110 bracket p 2 $

1102 bracket p 2 $

1111− if size sc > breakingSize then

1112− open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1113− st <> text "->" <+> prettySe 10 ((n, True):bnd) sc

1114− else

1115− open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1103+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1116− st <> text "->" <+> prettySe 10 ((n, True):bnd) sc

1104+ st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1117 | otherwise = prettySe 10 ((n, True):bnd) sc

1105 | otherwise = prettySe 10 ((n, True):bnd) sc

1118 where

1106 where

1119 st =

1107 st =

@@ -1122,18 +1110,11 @@ pprintPTerm impl bnd = prettySe 10 bnd

1122 _ -> empty

1110 _ -> empty

1123 prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1111 prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1124 bracket p 2 $

1112 bracket p 2 $

1125− if size sc > breakingSize then

1126− prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc

1113+ prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1127− else

1128− prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc

1129 prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =

1114 prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =

1130 bracket p 2 $

1115 bracket p 2 $

1131− if size sc > breakingSize then

1132− lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>

1133− rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc

1134− else

1135− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1116+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1136− rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc

1117+ rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1137 prettySe p bnd (PApp _ (PRef _ f) [])

1118 prettySe p bnd (PApp _ (PRef _ f) [])

1138 | not impl = prettyName impl bnd f

1119 | not impl = prettyName impl bnd f

1139 prettySe p bnd (PAppBind _ (PRef _ f) [])

1120 prettySe p bnd (PAppBind _ (PRef _ f) [])

@@ -1143,11 +1124,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

1143 , not (tnull nm) &&

1124 , not (tnull nm) &&

1144 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

1125 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

1145 let [l, r] = getExps args in

1126 let [l, r] = getExps args in

1146− bracket p 1 $

1127+ bracket p 1 . align . group $

1147− if size r > breakingSize then

1128+ (prettySe 1 bnd l <+> prettyName impl bnd op) <$> group (prettySe 0 bnd r)

1148− prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r

1149− else

1150− prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r

1151 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1129 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1152 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1130 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1153 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1131 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

@@ -1155,10 +1133,14 @@ pprintPTerm impl bnd = prettySe 10 bnd

1155 let args = getExps as

1133 let args = getExps as

1156 fp = prettySe 1 bnd f

1134 fp = prettySe 1 bnd f

1157 in

1135 in

1158− bracket p 1 $

1136+ bracket p 1 . group $

1159− hsep (if impl

1137+ if impl

1138+ then if null as

1139+ then fp

1160− then fp : map (prettyArgS bnd) as

1140+ else fp <+> align (vsep (map (prettyArgS bnd) as))

1141+ else if null args

1142+ then fp

1161− else fp : map (prettyArgSe bnd) args)

1143+ else fp <+> align (vsep (map (prettyArgSe bnd) args))

1162 prettySe p bnd (PCase _ scr opts) =

1144 prettySe p bnd (PCase _ scr opts) =

1163 text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody

1145 text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody

1164 where

1146 where

@@ -1171,32 +1153,18 @@ pprintPTerm impl bnd = prettySe 10 bnd

1171 prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1153 prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1172 prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

1154 prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

1173 prettySe p bnd (PEq _ l r) =

1155 prettySe p bnd (PEq _ l r) =

1174− bracket p 2 $

1156+ bracket p 2 . align . group $

1175− if size r > breakingSize then

1176− prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)

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

1177− else

1178− prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r

1179 where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

1158 where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

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

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

1181 bracket p 2 $

1160 bracket p 2 $

1182− if size r > breakingSize then

1183− text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)

1184− else

1185− text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1161+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1186 prettySe p bnd (PTyped l r) =

1162 prettySe p bnd (PTyped l r) =

1187 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1163 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1188 prettySe p bnd (PPair _ l r) =

1164 prettySe p bnd (PPair _ l r) =

1189− if size r > breakingSize then

1190− lparen <> prettySe 10 bnd l <> text "," <>

1191− line <> prettySe 10 bnd r <> rparen

1192− else

1193− lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen

1165+ lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen

1194 prettySe p bnd (PDPair _ l t r) =

1166 prettySe p bnd (PDPair _ l t r) =

1195− if size r > breakingSize then

1196− lparen <> prettySe 10 bnd l <+> text "**" <>

1197− line <> prettySe 10 bnd r <> rparen

1198− else

1199− lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1167+ lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1200 prettySe p bnd (PAlternative a as) =

1168 prettySe p bnd (PAlternative a as) =

1201 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1169 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1202 where

1170 where

src/Idris/Core/ProofState.hs+6−21

@@ -115,10 +115,7 @@ instance Show ProofState where

115

116instance Pretty ProofState OutputAnnotation where

117 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

118− if size nm > breakingSize then

119− pretty nm <+> colon <+> nest nestingSize (text " no more goals.")

120− else

121− pretty nm <+> colon <+> text " no more goals."

118+ pretty nm <+> colon <+> text " no more goals."

122 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =

119 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =

123 let OK g = goal (Just h) tm in

120 let OK g = goal (Just h) tm in

124 let wkEnv = premises g in

121 let wkEnv = premises g in

@@ -128,29 +125,17 @@ instance Pretty ProofState OutputAnnotation where

128 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)

125 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)

129 where

126 where

130 prettyGoal ps (Guess t v) =

127 prettyGoal ps (Guess t v) =

131− if size v > breakingSize then

132− prettyEnv ps t <+> text "=?=" <+>

133− nest nestingSize (prettyEnv ps v)

134− else

135− prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v

128+ prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v

136 prettyGoal ps b = prettyEnv ps $ binderTy b

129 prettyGoal ps b = prettyEnv ps $ binderTy b

137

130

138 prettyPs env [] = empty

131 prettyPs env [] = empty

139 prettyPs env ((n, Let t v):bs) =

132 prettyPs env ((n, Let t v):bs) =

140 nest nestingSize (pretty n <+> colon <+>

133 nest nestingSize (pretty n <+> colon <+>

141− if size v > breakingSize then

142− prettyEnv env t <+> text "=" <+>

143− nest nestingSize (prettyEnv env v) <+>

144− nest nestingSize (prettyPs env bs)

145− else

146− prettyEnv env t <+> text "=" <+> prettyEnv env v <+>

134+ prettyEnv env t <+> text "=" <+> prettyEnv env v <+>

147− nest nestingSize (prettyPs env bs))

135+ nest nestingSize (prettyPs env bs))

148 prettyPs env ((n, b):bs) =

136 prettyPs env ((n, b):bs) =

149− if size (binderTy b) > breakingSize then

150− nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)

137+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>

151− else

152− nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>

153− nest nestingSize (prettyPs env bs))

138+ nest nestingSize (prettyPs env bs))

154

139

155same Nothing n = True

140same Nothing n = True

156same (Just x) n = x == n

141same (Just x) n = x == n

src/Idris/Core/TT.hs+2−10

@@ -191,13 +191,8 @@ instance Show Err where

191instance Pretty Err OutputAnnotation where

192 pretty (Msg m) = text m

193 pretty (CantUnify _ l r e _ i) =

194− if size l + size r > breakingSize then

195− text "Cannot unify" <+> colon <+>

196− nest nestingSize (pretty l <+> text "and" <+> pretty r) <+>

197− nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

198− else

199 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

194 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

200− nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

195+ nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

201 pretty (ProviderError msg) = text msg

196 pretty (ProviderError msg) = text msg

202 pretty err@(LoadingFailed _ _) = text (show err)

197 pretty err@(LoadingFailed _ _) = text (show err)

203 pretty _ = text "Error"

198 pretty _ = text "Error"

@@ -210,10 +205,7 @@ type TC = TC' Err

210instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

205instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

211 pretty (OK ok) = pretty ok

206 pretty (OK ok) = pretty ok

212 pretty (Error err) =

207 pretty (Error err) =

213− if size err > breakingSize then

214− text "Error" <+> colon <+> (nest nestingSize $ pretty err)

215− else

216− text "Error" <+> colon <+> pretty err

208+ text "Error" <+> colon <+> pretty err

217

209

218instance Show a => Show (TC a) where

210instance Show a => Show (TC a) where

219 show (OK x) = show x

211 show (OK x) = show x

src/Idris/Prover.hs+13−10

@@ -89,18 +89,21 @@ elabStep st e = do case runStateT e st of

90dumpState :: IState -> ProofState -> Idris ()

91dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

92− iputGoal . renderPretty 0.7 breakingSize $

93− prettyName False [] nm <> colon <+> text "No more goals."

92+ do rendered <- iRender $ prettyName False [] nm <> colon <+> text "No more goals."

93+ iputGoal rendered

94dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

95 let OK ty = goalAtFocus ps

96 let OK env = envAtFocus ps

97− iputGoal . renderPretty 0.7 breakingSize $

98− prettyOtherGoals hs <> line <>

97+ let state = prettyOtherGoals hs <> line <>

99− prettyAssumptions env <> line <>

98+ prettyAssumptions env <> line <>

100− prettyGoal (zip (assumptionNames env) (repeat False)) ty

99+ prettyGoal (zip (assumptionNames env) (repeat False)) ty

100+ rendered <- iRender state

101+ iputGoal rendered

102+

101 where

103 where

102− -- XXX

104+ showImplicits = opt_showimp (idris_options ist)

105+

103− tPretty bnd t = pprintPTerm True bnd $ delab ist t

106+ tPretty bnd t = pprintPTerm showImplicits bnd $ delab ist t

104

107

105 assumptionNames :: Env -> [Name]

108 assumptionNames :: Env -> [Name]

106 assumptionNames = map fst

109 assumptionNames = map fst

@@ -113,14 +116,14 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = d

113 nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>

116 nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>

114 tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)

117 tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)

115 prettyPs bnd ((n, b) : bs) =

118 prettyPs bnd ((n, b) : bs) =

116− line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs

119+ line <> bindingOf n False <+> colon <+> align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs

117

120

118 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

121 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

119 prettyG bnd b = tPretty bnd $ binderTy b

122 prettyG bnd b = tPretty bnd $ binderTy b

120

123

121 prettyGoal bnd ty =

124 prettyGoal bnd ty =

122 text "---------- Goal: ----------" <$$>

125 text "---------- Goal: ----------" <$$>

123− bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)

126+ bindingOf h False <+> colon <+> align (prettyG bnd ty)

124

127

125 prettyAssumptions env =

128 prettyAssumptions env =

126 if length env == 0 then

129 if length env == 0 then

src/Idris/REPL.hs+22−18

@@ -14,7 +14,7 @@ import Idris.Parser

14import Idris.Primitives

15import Idris.Coverage

16import Idris.UnusedArgs

17−import Idris.Docs

17+import Idris.Docs hiding (Doc)

18import Idris.Help

19import Idris.Completion

20import qualified Idris.IdeSlave as IdeSlave

@@ -30,6 +30,7 @@ import Version_idris (gitHash)

30import Util.System

31import Util.DynamicLinker

32import Util.Net (listenOnLocalhost)

33+import Util.Pretty hiding ((</>))

34import Idris.Core.Evaluate

35import Idris.Core.Evaluate

35import Idris.Core.Execute (execute)

36import Idris.Core.Execute (execute)

@@ -470,32 +471,35 @@ process h fn (Check (PRef _ n))

470 = do ctxt <- getContext

471 = do ctxt <- getContext

471 ist <- getIState

472 ist <- getIState

472 imp <- impShow

473 imp <- impShow

473− c <- colourise

474 case lookupNames n ctxt of

475 ts@(t:_) ->

476 case lookup t (idris_metavars ist) of

477+ Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

477− Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

478+ showMetavarInfo imp ist n i

478 Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)

479 Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)

479 [] -> ihPrintError h $ "No such variable " ++ show n

480 [] -> ihPrintError h $ "No such variable " ++ show n

480 where

481 where

481− showMetavarInfo c imp ist n i

482+ showMetavarInfo imp ist n i

482 = case lookupTy n (tt_ctxt ist) of

483 = case lookupTy n (tt_ctxt ist) of

483− (ty:_) -> putTy c imp ist i (delab ist ty)

484+ (ty:_) -> putTy imp ist i [] (delab ist ty)

485+ putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

484− putTy c imp ist 0 sc = putGoal c imp ist sc

486+ putTy imp ist 0 bnd sc = putGoal imp ist bnd sc

485− putTy c imp ist i (PPi _ n t sc)

487+ putTy imp ist i bnd (PPi _ n t sc)

486− = let current = " " ++

488+ = let current = text " " <>

487 (case n of

489 (case n of

488− MN _ _ -> "_"

490+ MN _ _ -> text "_"

489− UN nm | ('_':'_':_) <- str nm -> "_"

491+ UN nm | ('_':'_':_) <- str nm -> text "_"

490− _ -> showName (Just ist) [] False c n) ++

492+ _ -> bindingOf n False) <+>

491− " : " ++ showTm ist t ++ "\n"

493+ colon <+> align (tPretty bnd ist t) <> line

492 in

494 in

493− current ++ putTy c imp ist (i-1) sc

495+ current <> putTy imp ist (i-1) ((n,False):bnd) sc

494− putTy c imp ist _ sc = putGoal c imp ist sc

496+ putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

495− putGoal c imp ist g

497+ putGoal imp ist bnd g

496− = "--------------------------------------\n" ++

498+ = text "--------------------------------------" <$>

497− showName (Just ist) [] False c n ++ " : " ++

499+ annotate (AnnName n Nothing Nothing) (text $ show n) <+> colon <+>

498− showTm ist g

500+ align (tPretty bnd ist g)

501+

502+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd t

499

503

500

504

501process h fn (Check t)

505process h fn (Check t)

src/Util/Pretty.hs+1−5

@@ -1,6 +1,6 @@

1module Util.Pretty (

2 module Text.PrettyPrint.Annotated.Leijen,

3− Sized(..), breakingSize, nestingSize,

3+ Sized(..), nestingSize,

4 Pretty(..)

5) where

@@ -17,10 +17,6 @@ instance (Sized a, Sized b) => Sized (a, b) where

17instance Sized a => Sized [a] where

18 size = sum . map size

20−-- The maximum size before we break on to another line.

21−breakingSize :: Int

22−breakingSize = 15

23−

24nestingSize :: Int

20nestingSize :: Int

25nestingSize = 1

21nestingSize = 1