git.iko.soy/Idris-dev
on master help sign in
Merge pull request #827 from david-christiansen/semantic-pprint

Pretty-printer updates

commit044ba305bd0a09ca9261e71b6a8c9f6fd0e5ce8b authorEdwin Brady <edwin.brady@gmail.com> dateSat 1 Feb 2014, 09:09 (13 years ago) parent50e3329106061d
7 files changed+117−146
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+27−4 src/Idris/AbsSyntaxTree.hs+46−78 src/Idris/Core/ProofState.hs+6−21 src/Idris/Core/TT.hs+2−10 src/Idris/Prover.hs+13−10 src/Idris/REPL.hs+22−18 src/Util/Pretty.hs+1−5
src/Idris/AbsSyntax.hs+27−4
@@ -407,6 +407,21 @@ getUndefined :: Idris [Name]
407407getUndefined = do i <- getIState
408408 return (map fst (idris_metavars i) \\ primDefs)
409409
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+
410425ihPrintResult :: Handle -> String -> Idris ()
411426ihPrintResult h s = do i <- getIState
412427 case idris_outputmode i of
@@ -420,15 +435,17 @@ ihPrintResult h s = do i <- getIState
420435-- | Write a pretty-printed term to the console with semantic coloring
421436consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
422437consoleDisplayAnnotated h output = do ist <- getIState
438+ rendered <- iRender $ output
423439 runIO . hPutStrLn h .
424− displayDecorated (consoleDecorate ist) .
425− renderCompact $ output
440+ displayDecorated (consoleDecorate ist) $
441+ rendered
442+
426443
427444-- | Write pretty-printed output to IDESlave with semantic annotations
428445ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
429446ideSlaveReturnAnnotated n h out = do ist <- getIState
430447 let (str, spans) = displaySpans .
431− renderCompact .
448+ renderPretty 0.8 80 .
432449 fmap (fancifyAnnots ist) $
433450 out
434451 good = [SymbolAtom "ok", toSExp str, toSExp spans]
@@ -451,7 +468,13 @@ ihPrintFunTypes h n overloads = do imp <- impShow
451468 RawOutput -> consoleDisplayAnnotated h output
452469 IdeSlave n -> ideSlaveReturnAnnotated n h output
453470 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
455478
456479fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
457480fancifyAnnots ist annot@(AnnName n _ _) =
src/Idris/AbsSyntaxTree.hs+46−78
@@ -22,7 +22,7 @@ import System.IO
2222import Control.Monad.Trans.State.Strict
2323import Control.Monad.Trans.Error
2424
25−import Data.List
25+import Data.List hiding (group)
2626import Data.Char
2727import qualified Data.Map as M
2828import qualified Data.Text as T
@@ -83,6 +83,10 @@ data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord
8383-- | The output mode in use
8484data OutputMode = RawOutput | IdeSlave Integer deriving Show
8585
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+
8690-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
8791-- without typechecking).
8892-- This will include all the functions and data declarations, plus fixity declarations
@@ -144,8 +148,8 @@ data IState = IState {
144148 idris_errorhandlers :: [Name], -- ^ Global error handlers
145149 idris_nameIdx :: (Int, Ctxt (Int, Name)),
146150 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
147− module_aliases :: M.Map [T.Text] [T.Text]
148−
151+ module_aliases :: M.Map [T.Text] [T.Text],
152+ idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
149153 }
150154
151155data SizeChange = Smaller | Same | Bigger | Unknown
@@ -215,6 +219,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
215219 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
216220 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
217221 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
222+ (ColsWide 80)
218223
219224-- | The monad for the main REPL - reading and processing files and updating
220225-- global state (hence the IO inner monad).
@@ -691,7 +696,6 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
691696deriving instance Binary PTactic'
692697deriving instance NFData PTactic'
693698!-}
694−
695699instance Sized a => Sized (PTactic' a) where
696700 size (Intro nms) = 1 + size nms
697701 size Intros = 1
@@ -1010,17 +1014,20 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
10101014
10111015-- Pretty-printing declarations and terms
10121016
1017+-- These "show" instances render to an absurdly wide screen because inserted line breaks
1018+-- could interfere with interactive editing, which calls "show".
1019+
10131020instance Show PTerm where
1014− showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm
1021+ showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm
10151022
10161023instance Show PDecl where
1017− showsPrec _ d = (displayS . renderCompact . showDeclImp False) d
1024+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d
10181025
10191026instance Show PClause where
1020− showsPrec _ c = (displayS . renderCompact . showCImp True) c
1027+ showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c
10211028
10221029instance Show PData where
1023− showsPrec _ d = (displayS . renderCompact . showDImp False) d
1030+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d
10241031
10251032instance Pretty PTerm OutputAnnotation where
10261033 pretty = prettyImp False
@@ -1060,9 +1067,6 @@ pprintPTerm impl bnd = prettySe 10 bnd
10601067 where
10611068 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
10621069 prettySe p bnd (PQuote r) =
1063− if size r > breakingSize then
1064− text "![" <> line <> pretty r <> text "]"
1065− else
10661070 text "![" <> pretty r <> text "]"
10671071 prettySe p bnd (PPatvar fc n) = pretty n
10681072 prettySe p bnd e
@@ -1070,35 +1074,23 @@ pprintPTerm impl bnd = prettySe 10 bnd
10701074 | Just n <- snat p e = annotate AnnConstData (text (show n))
10711075 prettySe p bnd (PRef fc n) = prettyName impl bnd n
10721076 prettySe p bnd (PLam n ty sc) =
1073− bracket p 2 $
1074− if size sc > breakingSize then
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
1077+ bracket p 2 . group . hang 2 $
1078+ text "\\" <> bindingOf n False <+> text "=>" <$>
1079+ prettySe 10 ((n, False):bnd) sc
10781080 prettySe p bnd (PLet n ty v sc) =
10791081 bracket p 2 $
1080− if size sc > breakingSize then
1081− text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>
1082− nest nestingSize (prettySe 10 ((n, False):bnd) sc)
1083− else
1084− text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>
1085− prettySe 10 ((n, False):bnd) sc
1082+ text "let" <+> bindingOf n False <+> text "=" </>
1083+ prettySe 10 bnd v <+> text "in" </>
1084+ prettySe 10 ((n, False):bnd) sc
10861085 prettySe p bnd (PPi (Exp l s _ _) n ty sc)
10871086 | n `elem` allNamesIn sc || impl =
10881087 let open = if Lazy `elem` l then text "|" <> lparen else lparen in
1089− bracket p 2 $
1090− if size sc > breakingSize then
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
1088+ bracket p 2 . group $
1089+ enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1090+ st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
10961091 | otherwise =
1097− bracket p 2 $
1098− if size sc > breakingSize then
1099− prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
1100− else
1101− prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
1092+ bracket p 2 . group $
1093+ group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
11021094 where
11031095 st =
11041096 case s of
@@ -1108,12 +1100,8 @@ pprintPTerm impl bnd = prettySe 10 bnd
11081100 | impl =
11091101 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in
11101102 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 <+>
1116− st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
1103+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1104+ st <> text "->" </> prettySe 10 ((n, True):bnd) sc
11171105 | otherwise = prettySe 10 ((n, True):bnd) sc
11181106 where
11191107 st =
@@ -1122,18 +1110,11 @@ pprintPTerm impl bnd = prettySe 10 bnd
11221110 _ -> empty
11231111 prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =
11241112 bracket p 2 $
1125− if size sc > breakingSize then
1126− 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
1113+ prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
11291114 prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =
11301115 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 <>
1136− rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc
1116+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1117+ rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
11371118 prettySe p bnd (PApp _ (PRef _ f) [])
11381119 | not impl = prettyName impl bnd f
11391120 prettySe p bnd (PAppBind _ (PRef _ f) [])
@@ -1143,11 +1124,8 @@ pprintPTerm impl bnd = prettySe 10 bnd
11431124 , not (tnull nm) &&
11441125 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
11451126 let [l, r] = getExps args in
1146− bracket p 1 $
1147− if size r > breakingSize then
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
1127+ bracket p 1 . align . group $
1128+ (prettySe 1 bnd l <+> prettyName impl bnd op) <$> group (prettySe 0 bnd r)
11511129 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
11521130 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
11531131 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
@@ -1155,10 +1133,14 @@ pprintPTerm impl bnd = prettySe 10 bnd
11551133 let args = getExps as
11561134 fp = prettySe 1 bnd f
11571135 in
1158− bracket p 1 $
1159− hsep (if impl
1160− then fp : map (prettyArgS bnd) as
1161− else fp : map (prettyArgSe bnd) args)
1136+ bracket p 1 . group $
1137+ if impl
1138+ then if null as
1139+ then fp
1140+ else fp <+> align (vsep (map (prettyArgS bnd) as))
1141+ else if null args
1142+ then fp
1143+ else fp <+> align (vsep (map (prettyArgSe bnd) args))
11621144 prettySe p bnd (PCase _ scr opts) =
11631145 text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody
11641146 where
@@ -1171,32 +1153,18 @@ pprintPTerm impl bnd = prettySe 10 bnd
11711153 prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
11721154 prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"
11731155 prettySe p bnd (PEq _ l r) =
1174− bracket p 2 $
1175− if size r > breakingSize then
1176− prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)
1177− else
1178− prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r
1156+ bracket p 2 . align . group $
1157+ prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
11791158 where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")
11801159 prettySe p bnd (PRewrite _ l r _) =
11811160 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
11861162 prettySe p bnd (PTyped l r) =
11871163 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
11881164 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
11941166 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
12001168 prettySe p bnd (PAlternative a as) =
12011169 lparen <> text "|" <> prettyAs <> text "|" <> rparen
12021170 where
src/Idris/Core/ProofState.hs+6−21
@@ -115,10 +115,7 @@ instance Show ProofState where
115115
116116instance Pretty ProofState OutputAnnotation where
117117 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."
122119 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =
123120 let OK g = goal (Just h) tm in
124121 let wkEnv = premises g in
@@ -128,29 +125,17 @@ instance Pretty ProofState OutputAnnotation where
128125 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
129126 where
130127 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
136129 prettyGoal ps b = prettyEnv ps $ binderTy b
137130
138131 prettyPs env [] = empty
139132 prettyPs env ((n, Let t v):bs) =
140133 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 <+>
147− nest nestingSize (prettyPs env bs))
134+ prettyEnv env t <+> text "=" <+> prettyEnv env v <+>
135+ nest nestingSize (prettyPs env bs))
148136 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)
151− else
152− nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
153− nest nestingSize (prettyPs env bs))
137+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
138+ nest nestingSize (prettyPs env bs))
154139
155140same Nothing n = True
156141same (Just x) n = x == n
src/Idris/Core/TT.hs+2−10
@@ -191,13 +191,8 @@ instance Show Err where
191191instance Pretty Err OutputAnnotation where
192192 pretty (Msg m) = text m
193193 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
199194 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))
201196 pretty (ProviderError msg) = text msg
202197 pretty err@(LoadingFailed _ _) = text (show err)
203198 pretty _ = text "Error"
@@ -210,10 +205,7 @@ type TC = TC' Err
210205instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where
211206 pretty (OK ok) = pretty ok
212207 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
217209
218210instance Show a => Show (TC a) where
219211 show (OK x) = show x
src/Idris/Prover.hs+13−10
@@ -89,18 +89,21 @@ elabStep st e = do case runStateT e st of
8989
9090dumpState :: IState -> ProofState -> Idris ()
9191dumpState 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
9494dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
9595 let OK ty = goalAtFocus ps
9696 let OK env = envAtFocus ps
97− iputGoal . renderPretty 0.7 breakingSize $
98− prettyOtherGoals hs <> line <>
99− prettyAssumptions env <> line <>
100− prettyGoal (zip (assumptionNames env) (repeat False)) ty
97+ let state = prettyOtherGoals hs <> line <>
98+ prettyAssumptions env <> line <>
99+ prettyGoal (zip (assumptionNames env) (repeat False)) ty
100+ rendered <- iRender state
101+ iputGoal rendered
102+
101103 where
102− -- XXX
103− tPretty bnd t = pprintPTerm True bnd $ delab ist t
104+ showImplicits = opt_showimp (idris_options ist)
105+
106+ tPretty bnd t = pprintPTerm showImplicits bnd $ delab ist t
104107
105108 assumptionNames :: Env -> [Name]
106109 assumptionNames = map fst
@@ -113,14 +116,14 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = d
113116 nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>
114117 tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)
115118 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
117120
118121 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
119122 prettyG bnd b = tPretty bnd $ binderTy b
120123
121124 prettyGoal bnd ty =
122125 text "---------- Goal: ----------" <$$>
123− bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)
126+ bindingOf h False <+> colon <+> align (prettyG bnd ty)
124127
125128 prettyAssumptions env =
126129 if length env == 0 then
src/Idris/REPL.hs+22−18
@@ -14,7 +14,7 @@ import Idris.Parser
1414import Idris.Primitives
1515import Idris.Coverage
1616import Idris.UnusedArgs
17−import Idris.Docs
17+import Idris.Docs hiding (Doc)
1818import Idris.Help
1919import Idris.Completion
2020import qualified Idris.IdeSlave as IdeSlave
@@ -30,6 +30,7 @@ import Version_idris (gitHash)
3030import Util.System
3131import Util.DynamicLinker
3232import Util.Net (listenOnLocalhost)
33+import Util.Pretty hiding ((</>))
3334
3435import Idris.Core.Evaluate
3536import Idris.Core.Execute (execute)
@@ -470,32 +471,35 @@ process h fn (Check (PRef _ n))
470471 = do ctxt <- getContext
471472 ist <- getIState
472473 imp <- impShow
473− c <- colourise
474474 case lookupNames n ctxt of
475475 ts@(t:_) ->
476476 case lookup t (idris_metavars ist) of
477− Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
477+ Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
478+ showMetavarInfo imp ist n i
478479 Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)
479480 [] -> ihPrintError h $ "No such variable " ++ show n
480481 where
481− showMetavarInfo c imp ist n i
482+ showMetavarInfo imp ist n i
482483 = case lookupTy n (tt_ctxt ist) of
483− (ty:_) -> putTy c imp ist i (delab ist ty)
484− putTy c imp ist 0 sc = putGoal c imp ist sc
485− putTy c imp ist i (PPi _ n t sc)
486− = let current = " " ++
484+ (ty:_) -> putTy imp ist i [] (delab ist ty)
485+ putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
486+ putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
487+ putTy imp ist i bnd (PPi _ n t sc)
488+ = let current = text " " <>
487489 (case n of
488− MN _ _ -> "_"
489− UN nm | ('_':'_':_) <- str nm -> "_"
490− _ -> showName (Just ist) [] False c n) ++
491− " : " ++ showTm ist t ++ "\n"
490+ MN _ _ -> text "_"
491+ UN nm | ('_':'_':_) <- str nm -> text "_"
492+ _ -> bindingOf n False) <+>
493+ colon <+> align (tPretty bnd ist t) <> line
492494 in
493− current ++ putTy c imp ist (i-1) sc
494− putTy c imp ist _ sc = putGoal c imp ist sc
495− putGoal c imp ist g
496− = "--------------------------------------\n" ++
497− showName (Just ist) [] False c n ++ " : " ++
498− showTm ist g
495+ current <> putTy imp ist (i-1) ((n,False):bnd) sc
496+ putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc
497+ putGoal imp ist bnd g
498+ = text "--------------------------------------" <$>
499+ annotate (AnnName n Nothing Nothing) (text $ show n) <+> colon <+>
500+ align (tPretty bnd ist g)
501+
502+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd t
499503
500504
501505process h fn (Check t)
src/Util/Pretty.hs+1−5
@@ -1,6 +1,6 @@
11module Util.Pretty (
22 module Text.PrettyPrint.Annotated.Leijen,
3− Sized(..), breakingSize, nestingSize,
3+ Sized(..), nestingSize,
44 Pretty(..)
55) where
66
@@ -17,10 +17,6 @@ instance (Sized a, Sized b) => Sized (a, b) where
1717instance Sized a => Sized [a] where
1818 size = sum . map size
1919
20−-- The maximum size before we break on to another line.
21−breakingSize :: Int
22−breakingSize = 15
23−
2420nestingSize :: Int
2521nestingSize = 1
2622