da24632 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Render using console width

commitda24632cafc534d24fb0c07842509142931bfd97 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 31 Jan 2014, 19:42 (13 years ago) parent94c4cf8

3 files changed+37−13

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+20−3 src/Idris/AbsSyntaxTree.hs+7−2 src/Idris/Prover.hs+10−8

src/Idris/AbsSyntax.hs+20−3

@@ -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 -> renderCompact d

421+ ColsWide n -> if n < 1

422+ then renderCompact 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,9 +435,11 @@ 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 ()

@@ -451,7 +468,7 @@ 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)

455472

456473fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

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

src/Idris/AbsSyntaxTree.hs+7−2

@@ -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).

src/Idris/Prover.hs+10−8

@@ -89,15 +89,17 @@ 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

102104 showImplicits = opt_showimp (idris_options ist)

103105

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

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

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

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

117− 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

118120

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

120122 prettyG bnd b = tPretty bnd $ binderTy b

121123

122124 prettyGoal bnd ty =

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

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

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

125127

126128 prettyAssumptions env =

127129 if length env == 0 then