544546d · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -24,6 +24,8 @@ New in 0.9.11:

24 structurally smaller than "(x :: xs)"

25* assert_total internal function, which marks a subexpression as assumed to

26 be total, e.g "assert_total (tail (x :: xs))".

27+* Terminal width is automatically detected if Idris is compiled with curses

28+ support. If curses is not available, automatic mode assumes 80 columns.

27

29

28Internal changes

30Internal changes

29

31

custom.mk-alldeps+1−1

@@ -1,2 +1,2 @@

1−CABALFLAGS += -f LLVM -f FFI

1+CABALFLAGS += -f LLVM -f FFI -f curses

2

idris.cabal+9

@@ -370,6 +370,11 @@ Flag GMP

370 Default: False

371 manual: True

372

373+Flag curses

374+ Description: Use Curses to get the screen width

375+ Default: False

376+ manual: True

377+

373-- This flag determines whether to show Git hashes in version strings

378-- This flag determines whether to show Git hashes in version strings

374-- Defaults to True because Hackage is a source release

379-- Defaults to True because Hackage is a source release

375Flag release

380Flag release

@@ -449,6 +454,7 @@ Library

449

454

450 , Pkg.Package

455 , Pkg.Package

451 , Util.DynamicLinker

456 , Util.DynamicLinker

457+ , Util.ScreenSize

452

458

453 Other-modules:

459 Other-modules:

454 Util.Pretty

460 Util.Pretty

@@ -529,6 +535,9 @@ Library

529 if flag(GMP)

535 if flag(GMP)

530 build-depends: libffi

536 build-depends: libffi

531 cpp-options: -DIDRIS_GMP

537 cpp-options: -DIDRIS_GMP

538+ if flag(curses)

539+ build-depends: hscurses

540+ cpp-options: -DCURSES

532

541

533Executable idris

542Executable idris

534 Main-is: Main.hs

543 Main-is: Main.hs

src/Idris/AbsSyntax.hs+17−5

@@ -36,6 +36,7 @@ import Control.Monad.Error (throwError, catchError)

36import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)

37

38import Util.Pretty

39+import Util.ScreenSize

39import Util.System

40import Util.System

40

41

41getContext :: Idris Context

42getContext :: Idris Context

@@ -414,13 +415,24 @@ setWidth :: ConsoleWidth -> Idris ()

414setWidth w = do ist <- getIState

415setWidth w = do ist <- getIState

415 put ist { idris_consolewidth = w }

416 put ist { idris_consolewidth = w }

416

417

418+renderWidth :: Idris Int

419+renderWidth = do iw <- getWidth

420+ case iw of

421+ InfinitelyWide -> return 100000000

422+ ColsWide n -> return (max n 1)

423+ AutomaticWidth -> runIO getScreenWidth

424+

425+

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

426iRender :: Doc a -> Idris (SimpleDoc a)

418iRender d = do w <- getWidth

427iRender d = do w <- getWidth

419− return $ case w of

428+ case w of

420− InfinitelyWide -> renderPretty 1.0 1000000000 d

429+ InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

421− ColsWide n -> if n < 1

430+ ColsWide n -> return $

431+ if n < 1

422− then renderPretty 1.0 1000000000 d

432+ then renderPretty 1.0 1000000000 d

423− else renderPretty 0.5 n d

433+ else renderPretty 0.8 n d

434+ AutomaticWidth -> do width <- runIO getScreenWidth

435+ return $ renderPretty 0.8 width d

424

436

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

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

426ihPrintResult h s = do i <- getIState

438ihPrintResult h s = do i <- getIState

src/Idris/AbsSyntaxTree.hs+14−7

@@ -85,7 +85,8 @@ data OutputMode = RawOutput | IdeSlave Integer deriving Show

85

86-- | How wide is the console?

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

88− | ColsWide Int -- ^ Must be positive

88+ | ColsWide Int -- ^ Manually specified - must be positive

89+ | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

89

90

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

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

91-- without typechecking).

92-- without typechecking).

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

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

220 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

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

221 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

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

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

222− (ColsWide 80)

223+ AutomaticWidth

223

224

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

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

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

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

@@ -283,6 +284,7 @@ data Command = Quit

283 | ColourOn

284 | ColourOn

284 | ColourOff

285 | ColourOff

285 | ListErrorHandlers

286 | ListErrorHandlers

287+ | SetConsoleWidth ConsoleWidth

286

288

287data Opt = Filename String

289data Opt = Filename String

288 | Ver

290 | Ver

@@ -330,6 +332,7 @@ data Opt = Filename String

330 | OptLevel Word

332 | OptLevel Word

331 | Client String

333 | Client String

332 | ShowOrigErr

334 | ShowOrigErr

335+ | AutoWidth -- ^ Automatically adjust terminal width

333 deriving (Show, Eq)

336 deriving (Show, Eq)

334

337

335-- Parsed declarations

338-- Parsed declarations

@@ -1208,6 +1211,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

1208

1211

1209 slist' p bnd (PApp _ (PRef _ nil) _)

1212 slist' p bnd (PApp _ (PRef _ nil) _)

1210 | not impl && nsroot nil == sUN "Nil" = Just []

1213 | not impl && nsroot nil == sUN "Nil" = Just []

1214+ slist' p bnd (PRef _ nil)

1215+ | not impl && nsroot nil == sUN "Nil" = Just []

1211 slist' p bnd (PApp _ (PRef _ cons) args)

1216 slist' p bnd (PApp _ (PRef _ cons) args)

1212 | nsroot cons == sUN "::",

1217 | nsroot cons == sUN "::",

1213 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1218 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

@@ -1217,14 +1222,16 @@ pprintPTerm impl bnd = prettySe 10 bnd

1217 where

1222 where

1218 isImp (PImp {}) = True

1223 isImp (PImp {}) = True

1219 isImp _ = False

1224 isImp _ = False

1220− slist' _ _ _ = Nothing

1225+ slist' _ _ tm = Nothing

1221

1226

1222 slist p bnd e | Just es <- slist' p bnd e = Just $

1227 slist p bnd e | Just es <- slist' p bnd e = Just $

1223 case es of [] -> annotate AnnConstData $ text "[]"

1228 case es of [] -> annotate AnnConstData $ text "[]"

1224− [x] -> enclose left

1229+ [x] -> enclose left right . group $

1225− right

1226− (prettySe p bnd x)

1230+ prettySe p bnd x

1227− xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs

1231+ xs -> (enclose left right .

1232+ align . group . vsep .

1233+ punctuate comma .

1234+ map (prettySe p bnd)) xs

1228 where left = (annotate AnnConstData (text "["))

1235 where left = (annotate AnnConstData (text "["))

1229 right = (annotate AnnConstData (text "]"))

1236 right = (annotate AnnConstData (text "]"))

1230 comma = (annotate AnnConstData (text ","))

1237 comma = (annotate AnnConstData (text ","))

src/Idris/Completion.hs+6−1

@@ -54,7 +54,7 @@ tactics = map fst tacticArgs

54-- | Convert a name into a string usable for completion. Filters out names

55-- that users probably don't want to see.

56nameString :: Name -> Maybe String

57−nameString (UN nm)

57+nameString (UN nm)

58 | not (tnull nm) && (thead nm == '@' || thead nm == '#') = Nothing

59nameString (UN n) = Just (str n)

60nameString (NS n _) = nameString n

@@ -106,6 +106,10 @@ completeOption :: CompletionFunc Idris

106completeOption = completeWord Nothing " \t" completeOpt

107 where completeOpt = return . completeWith ["errorcontext", "showimplicits", "originalerrors"]

108

109+completeConsoleWidth :: CompletionFunc Idris

110+completeConsoleWidth = completeWord Nothing " \t" completeW

111+ where completeW = return . completeWith ["auto", "infinite", "80", "120"]

112+

109isWhitespace :: Char -> Bool

113isWhitespace :: Char -> Bool

110isWhitespace = (flip elem) " \t\n"

114isWhitespace = (flip elem) " \t\n"

111

115

@@ -152,6 +156,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo

152 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name

156 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name

153 completeArg ColourArg = completeColour (prev, next)

157 completeArg ColourArg = completeColour (prev, next)

154 completeArg NoArg = noCompletion (prev, next)

158 completeArg NoArg = noCompletion (prev, next)

159+ completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)

155 completeCmdName = return $ ("", completeWith commands cmd)

160 completeCmdName = return $ ("", completeWith commands cmd)

156

161

157-- | Complete REPL commands and defined identifiers

162-- | Complete REPL commands and defined identifiers

src/Idris/Help.hs+3

@@ -9,6 +9,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression

9 | ColourArg -- ^ The command is the colour-setting command

10 | NoArg -- ^ No completion (yet!?)

11 | SpecialHeaderArg -- ^ do not use

12+ | ConsoleWidthArg -- ^ The width of the console

12

13

13instance Show CmdArg where

14instance Show CmdArg where

14 show ExprArg = "<expr>"

15 show ExprArg = "<expr>"

@@ -20,6 +21,7 @@ instance Show CmdArg where

20 show ColourArg = "<option>"

21 show ColourArg = "<option>"

21 show NoArg = ""

22 show NoArg = ""

22 show SpecialHeaderArg = "Arguments"

23 show SpecialHeaderArg = "Arguments"

24+ show ConsoleWidthArg = "auto|infinite|<number>"

23

25

24help :: [([String], CmdArg, String)]

26help :: [([String], CmdArg, String)]

25help =

27help =

@@ -50,6 +52,7 @@ help =

50 ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),

52 ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),

51 ([":unset"], OptionArg, "Unset an option"),

53 ([":unset"], OptionArg, "Unset an option"),

52 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

54 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

55+ ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

53 ([":q",":quit"], NoArg, "Exit the Idris system")

56 ([":q",":quit"], NoArg, "Exit the Idris system")

54 ]

57 ]

55

58

src/Idris/REPL.hs+2

@@ -935,6 +935,8 @@ process h fn ListErrorHandlers =

935 [] -> iPrintResult "No registered error handlers"

936 handlers ->

937 iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

938+process h fn (SetConsoleWidth w) = setWidth w

939+

938

940

939classInfo :: ClassInfo -> Idris ()

941classInfo :: ClassInfo -> Idris ()

940classInfo ci = do iputStrLn "Methods:\n"

942classInfo ci = do iputStrLn "Methods:\n"

src/Idris/REPLParser.hs+6

@@ -97,6 +97,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

97 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))

98 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

99 <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)

100+ <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))

100 <|> do P.whiteSpace; do eof; return NOP

101 <|> do P.whiteSpace; do eof; return NOP

101 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

102 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

102

103

@@ -107,6 +108,11 @@ pOption = do discard (P.symbol "errorcontext"); return ErrContext

107 <|> do discard (P.symbol "showimplicits"); return ShowImpl

108 <|> do discard (P.symbol "showimplicits"); return ShowImpl

108 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

109 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

109

110

111+pConsoleWidth :: P.IdrisParser ConsoleWidth

112+pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

113+ <|> do discard (P.symbol "infinite"); return InfinitelyWide

114+ <|> do n <- fmap fromInteger P.natural; return (ColsWide n)

115+

110colours :: [(String, Maybe Color)]

116colours :: [(String, Maybe Color)]

111colours = [ ("black", Just Black)

117colours = [ ("black", Just Black)

112 , ("red", Just Red)

118 , ("red", Just Red)

src/Util/ScreenSize.hsnew file+21

@@ -0,0 +1,21 @@

1+{-# LANGUAGE CPP #-}

2+module Util.ScreenSize where

3+

4+import Debug.Trace

5+

6+#ifndef CURSES

7+

8+getScreenWidth :: IO Int

9+getScreenWidth = return 80

10+

11+#else

12+

13+import UI.HSCurses.Curses

14+

15+getScreenWidth :: IO Int

16+getScreenWidth = do initScr

17+ refresh

18+ size <- scrSize

19+ endWin

20+ return (snd size)

21+#endif