1bf2731 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

issue #2004 resolved by --consolewith cmd line param

1bf2731Andreas Reuleaux12 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -801,6 +801,7 @@ Library

801 , vector-binary-instances < 0.3

802 , xml < 1.4

803 , zlib < 0.6

804+ , safe

804 Extensions: MultiParamTypeClasses

805 Extensions: MultiParamTypeClasses

805 , DeriveFoldable

806 , DeriveFoldable

806 , DeriveTraversable

807 , DeriveTraversable

src/Idris/AbsSyntaxTree.hs+24−21

@@ -66,27 +66,27 @@ toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not impleme

66eInfoNames :: ElabInfo -> [Name]

67eInfoNames info = map fst (params info) ++ M.keys (inblock info)

69−data IOption = IOption { opt_logLevel :: Int,

69+data IOption = IOption { opt_logLevel :: Int,

70− opt_typecase :: Bool,

70+ opt_typecase :: Bool,

71− opt_typeintype :: Bool,

71+ opt_typeintype :: Bool,

72− opt_coverage :: Bool,

72+ opt_coverage :: Bool,

73− opt_showimp :: Bool, -- ^^ show implicits

73+ opt_showimp :: Bool, -- ^^ show implicits

74− opt_errContext :: Bool,

74+ opt_errContext :: Bool,

75− opt_repl :: Bool,

75+ opt_repl :: Bool,

76− opt_verbose :: Bool,

76+ opt_verbose :: Bool,

77− opt_nobanner :: Bool,

77+ opt_nobanner :: Bool,

78− opt_quiet :: Bool,

78+ opt_quiet :: Bool,

79− opt_codegen :: Codegen,

79+ opt_codegen :: Codegen,

80− opt_outputTy :: OutputType,

80+ opt_outputTy :: OutputType,

81− opt_ibcsubdir :: FilePath,

81+ opt_ibcsubdir :: FilePath,

82− opt_importdirs :: [FilePath],

82+ opt_importdirs :: [FilePath],

83− opt_triple :: String,

83+ opt_triple :: String,

84− opt_cpu :: String,

84+ opt_cpu :: String,

85− opt_cmdline :: [Opt], -- remember whole command line

85+ opt_cmdline :: [Opt], -- remember whole command line

86− opt_origerr :: Bool,

86+ opt_origerr :: Bool,

87− opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

87+ opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

88− opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

88+ opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

89− opt_optimise :: [Optimisation]

89+ opt_optimise :: [Optimisation]

90 }

91 deriving (Show, Eq)

@@ -151,6 +151,8 @@ data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

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

152 | ColsWide Int -- ^ Manually specified - must be positive

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

154+ deriving (Show, Eq)

155+

154

156

155-- | The global state used in the Idris monad

157-- | The global state used in the Idris monad

156data IState = IState {

158data IState = IState {

@@ -463,6 +465,7 @@ data Opt = Filename String

463 | ShowOrigErr

465 | ShowOrigErr

464 | AutoWidth -- ^ Automatically adjust terminal width

466 | AutoWidth -- ^ Automatically adjust terminal width

465 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

467 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

468+ | UseConsoleWidth ConsoleWidth

466 deriving (Show, Eq)

469 deriving (Show, Eq)

467

470

468-- Parsed declarations

471-- Parsed declarations

src/Idris/CmdOptions.hs+30

@@ -11,6 +11,12 @@ import Options.Applicative.Arrows

11import Data.Char

12import Data.Maybe

14+import Text.ParserCombinators.ReadP hiding (many, option)

15+

16+import Safe (lastMay)

17+

18+

19+

14import qualified Text.PrettyPrint.ANSI.Leijen as PP

20import qualified Text.PrettyPrint.ANSI.Leijen as PP

16runArgParser :: IO [Opt]

22runArgParser :: IO [Opt]

@@ -67,6 +73,7 @@ parser = runA $ proc () -> do

67 files <- asA (many $ argument (fmap Filename str) (metavar "FILES")) -< ()

73 files <- asA (many $ argument (fmap Filename str) (metavar "FILES")) -< ()

68 A parseVersion >>> A helper -< (flags ++ files)

74 A parseVersion >>> A helper -< (flags ++ files)

76+

70parseFlags :: Parser [Opt]

77parseFlags :: Parser [Opt]

71parseFlags = many $

78parseFlags = many $

72 flag' NoBanner (long "nobanner" <> help "Suppress the banner")

79 flag' NoBanner (long "nobanner" <> help "Suppress the banner")

@@ -132,6 +139,10 @@ parseFlags = many $

132 <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

139 <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

133 <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

140 <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

134 <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")

141 <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")

142+

143+ <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

144+

145+

135 where

146 where

136 getExt s = case maybeRead s of

147 getExt s = case maybeRead s of

137 Just ext -> ext

148 Just ext -> ext

@@ -151,3 +162,22 @@ preProcOpts (x:xs) ys = preProcOpts xs (x:ys)

151parseCodegen :: String -> Codegen

162parseCodegen :: String -> Codegen

152parseCodegen "bytecode" = Bytecode

163parseCodegen "bytecode" = Bytecode

153parseCodegen cg = Via (map toLower cg)

164parseCodegen cg = Via (map toLower cg)

165+

166+

167+

168+

169+parseConsoleWidth :: Monad m => String -> m ConsoleWidth

170+parseConsoleWidth "auto" = return AutomaticWidth

171+parseConsoleWidth "infinite" = return InfinitelyWide

172+parseConsoleWidth s =

173+ case lastMay (readP_to_S (integerReader) s) of

174+ Just (r, _) -> return $ ColsWide r

175+ _ -> fail $ "Cannot parse: " ++ s

176+

177+

178+

179+integerReader :: ReadP Int

180+integerReader = do

181+ digits <- many1 $ satisfy isDigit

182+ return $ read digits

183+

src/Idris/REPL.hs+9−1

@@ -1554,7 +1554,9 @@ idrisMain opts =

1554 when (DefaultTotal `elem` opts) $ do i <- getIState

1555 putIState (i { default_total = True })

1556 setColourise $ not quiet && last (True : opt getColour opts)

1557+

1557− when (not runrepl) $ setWidth InfinitelyWide

1558+ when (not runrepl) $ mapM_ setWidth (opt getConsoleWidth opts)

1559+

1558 mapM_ addLangExt (opt getLanguageExt opts)

1560 mapM_ addLangExt (opt getLanguageExt opts)

1559 setREPL runrepl

1561 setREPL runrepl

1560 setQuiet (quiet || isJust script || not (null immediate))

1562 setQuiet (quiet || isJust script || not (null immediate))

@@ -1777,6 +1779,12 @@ getCodegen :: Opt -> Maybe Codegen

1777getCodegen (UseCodegen x) = Just x

1779getCodegen (UseCodegen x) = Just x

1778getCodegen _ = Nothing

1780getCodegen _ = Nothing

1779

1781

1782+

1783+getConsoleWidth :: Opt -> Maybe ConsoleWidth

1784+getConsoleWidth (UseConsoleWidth x) = Just x

1785+getConsoleWidth _ = Nothing

1786+

1787+

1780getExecScript :: Opt -> Maybe String

1788getExecScript :: Opt -> Maybe String

1781getExecScript (InterpretScript expr) = Just expr

1789getExecScript (InterpretScript expr) = Just expr

1782getExecScript _ = Nothing

1790getExecScript _ = Nothing

test/docs001/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --nobanner --nocolor docs001.idr < input

2+idris --nobanner --nocolor --consolewidth 80 docs001.idr < input

3rm *.ibc