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

git.iko.soy/Idris-dev

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

Automatically detect console width + fix pretty-printing of no-argument Nil constructors

commit544546de4ab368b72eed686301bd781aea01fef2 authorEdwin Brady <edwin.brady@gmail.com> dateSun 2 Feb 2014, 15:03 (13 years ago) parent63d2989 28ffcf8

10 files changed+81−14

compare with master

unifiedsplit

CHANGELOG+2 custom.mk-alldeps+1−1 idris.cabal+9 src/Idris/AbsSyntax.hs+17−5 src/Idris/AbsSyntaxTree.hs+14−7 src/Idris/Completion.hs+6−1 src/Idris/Help.hs+3 src/Idris/REPL.hs+2 src/Idris/REPLParser.hs+6 src/Util/ScreenSize.hs+21

CHANGELOG+2

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

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

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

2626 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.

2729

2830Internal changes

2931

custom.mk-alldeps+1−1

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

1−CABALFLAGS += -f LLVM -f FFI

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

idris.cabal+9

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

370370 Default: False

371371 manual: True

372372

373+Flag curses

374+ Description: Use Curses to get the screen width

375+ Default: False

376+ manual: True

377+

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

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

375380Flag release

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

449454

450455 , Pkg.Package

451456 , Util.DynamicLinker

457+ , Util.ScreenSize

452458

453459 Other-modules:

454460 Util.Pretty

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

529535 if flag(GMP)

530536 build-depends: libffi

531537 cpp-options: -DIDRIS_GMP

538+ if flag(curses)

539+ build-depends: hscurses

540+ cpp-options: -DCURSES

532541

533542Executable idris

534543 Main-is: Main.hs

src/Idris/AbsSyntax.hs+17−5

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

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

3737

3838import Util.Pretty

39+import Util.ScreenSize

3940import Util.System

4041

4142getContext :: Idris Context

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

414415setWidth w = do ist <- getIState

415416 put ist { idris_consolewidth = w }

416417

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+

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

418427iRender 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

428+ case w of

429+ InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

430+ ColsWide n -> return $

431+ if n < 1

432+ then renderPretty 1.0 1000000000 d

433+ else renderPretty 0.8 n d

434+ AutomaticWidth -> do width <- runIO getScreenWidth

435+ return $ renderPretty 0.8 width d

424436

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

426438ihPrintResult h s = do i <- getIState

src/Idris/AbsSyntaxTree.hs+14−7

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

8585

8686-- | How wide is the console?

8787data 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

8990

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

9192-- without typechecking).

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

219220 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

220221 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

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

222− (ColsWide 80)

223+ AutomaticWidth

223224

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

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

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

283284 | ColourOn

284285 | ColourOff

285286 | ListErrorHandlers

287+ | SetConsoleWidth ConsoleWidth

286288

287289data Opt = Filename String

288290 | Ver

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

330332 | OptLevel Word

331333 | Client String

332334 | ShowOrigErr

335+ | AutoWidth -- ^ Automatically adjust terminal width

333336 deriving (Show, Eq)

334337

335338-- Parsed declarations

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

12081211

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

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

1214+ slist' p bnd (PRef _ nil)

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

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

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

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

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

12171222 where

12181223 isImp (PImp {}) = True

12191224 isImp _ = False

1220− slist' _ _ _ = Nothing

1225+ slist' _ _ tm = Nothing

12211226

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

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

1224− [x] -> enclose left

1225− right

1226− (prettySe p bnd x)

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

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

1230+ prettySe p bnd x

1231+ xs -> (enclose left right .

1232+ align . group . vsep .

1233+ punctuate comma .

1234+ map (prettySe p bnd)) xs

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

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

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

src/Idris/Completion.hs+6−1

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

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

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

5656nameString :: Name -> Maybe String

57−nameString (UN nm)

57+nameString (UN nm)

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

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

6060nameString (NS n _) = nameString n

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

106106completeOption = completeWord Nothing " \t" completeOpt

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

108108

109+completeConsoleWidth :: CompletionFunc Idris

110+completeConsoleWidth = completeWord Nothing " \t" completeW

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

112+

109113isWhitespace :: Char -> Bool

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

111115

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

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

153157 completeArg ColourArg = completeColour (prev, next)

154158 completeArg NoArg = noCompletion (prev, next)

159+ completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)

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

156161

157162-- | Complete REPL commands and defined identifiers

src/Idris/Help.hs+3

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

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

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

1111 | SpecialHeaderArg -- ^ do not use

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

1213

1314instance Show CmdArg where

1415 show ExprArg = "<expr>"

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

2021 show ColourArg = "<option>"

2122 show NoArg = ""

2223 show SpecialHeaderArg = "Arguments"

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

2325

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

2527help =

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

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

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

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

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

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

5457 ]

5558

src/Idris/REPL.hs+2

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

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

936936 handlers ->

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

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

939+

938940

939941classInfo :: ClassInfo -> Idris ()

940942classInfo 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)

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

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

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

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

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

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

102103

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

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

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

109110

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+

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

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

112118 , ("red", Just Red)

src/Util/ScreenSize.hsnew file+21

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

1+{-# LANGUAGE CPP #-}

2+module Util.ScreenSize where

4+import Debug.Trace

6+#ifndef CURSES

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