da24632 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Render using console width

da24632David Raymond Christiansen13 years ago

src/Idris/AbsSyntax.hs+20−3

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

421+ ColsWide n -> if n < 1

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

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

455

472

456fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

473fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

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

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

src/Idris/AbsSyntaxTree.hs+7−2

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

src/Idris/Prover.hs+10−8

@@ -89,15 +89,17 @@ 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 showImplicits = opt_showimp (idris_options ist)

104 showImplicits = opt_showimp (idris_options ist)

103

105

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

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

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

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

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

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

118 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

118

120

119 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

120 prettyG bnd b = tPretty bnd $ binderTy b

122 prettyG bnd b = tPretty bnd $ binderTy b

121

123

122 prettyGoal bnd ty =

124 prettyGoal bnd ty =

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

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

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

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

125

127

126 prettyAssumptions env =

128 prettyAssumptions env =

127 if length env == 0 then

129 if length env == 0 then