228ffdb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

quiet mode: for editors

commit228ffdb3df0b7399de4e9ddd1fa6c75dd0ec2752 authorraichoo <raichoo@googlemail.com> dateWed 20 Mar 2013, 17:03 (14 years ago) parent9f1141e

4 files changed+33−16

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6 src/Idris/AbsSyntaxTree.hs+13−11 src/Idris/REPL.hs+13−5 src/Main.hs+1

src/Idris/AbsSyntax.hs+6

@@ -279,6 +279,12 @@ setREPL t = do i <- getIState

279279 let opt' = opts { opt_repl = t }

280280 putIState $ i { idris_options = opt' }

281281

282+setQuiet :: Bool -> Idris ()

283+setQuiet q = do i <- getIState

284+ let opts = idris_options i

285+ let opt' = opts { opt_quiet = q }

286+ putIState $ i { idris_options = opt' }

287+

282288setTarget :: Target -> Idris ()

283289setTarget t = do i <- getIState

284290 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+13−11

@@ -23,23 +23,24 @@ import Data.Either

2323

2424import Debug.Trace

2525

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

27− opt_typecase :: Bool,

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

27+ opt_typecase :: Bool,

2828 opt_typeintype :: Bool,

29− opt_coverage :: Bool,

30− opt_showimp :: Bool,

29+ opt_coverage :: Bool,

30+ opt_showimp :: Bool,

3131 opt_errContext :: Bool,

32− opt_repl :: Bool,

33− opt_verbose :: Bool,

34− opt_target :: Target,

35− opt_outputTy :: OutputType,

36− opt_ibcsubdir :: FilePath,

32+ opt_repl :: Bool,

33+ opt_verbose :: Bool,

34+ opt_quiet :: Bool,

35+ opt_target :: Target,

36+ opt_outputTy :: OutputType,

37+ opt_ibcsubdir :: FilePath,

3738 opt_importdirs :: [FilePath],

38− opt_cmdline :: [Opt] -- remember whole command line

39+ opt_cmdline :: [Opt] -- remember whole command line

3940 }

4041 deriving (Show, Eq)

4142

42−defaultOpts = IOption 0 False False True False False True True ViaC Executable "" [] []

43+defaultOpts = IOption 0 False False True False False True True False ViaC Executable "" [] []

4344

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

4546-- without typechecking).

@@ -190,6 +191,7 @@ data Command = Quit

190191data Opt = Filename String

191192 | Ver

192193 | Usage

194+ | Quiet

193195 | ShowLibs

194196 | ShowLibdir

195197 | ShowIncs

src/Idris/REPL.hs+13−5

@@ -57,10 +57,13 @@ repl :: IState -- ^ The initial state

5757 -> InputT Idris ()

5858repl orig mods

5959 = H.catch

60− (do let prompt = mkPrompt mods

61− x <- getInputLine (prompt ++ "> ")

60+ (do let quiet = opt_quiet (idris_options orig)

61+ let prompt = if quiet

62+ then ""

63+ else mkPrompt mods ++ "> "

64+ x <- getInputLine prompt

6265 case x of

63− Nothing -> do lift $ iputStrLn "Bye bye"

66+ Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

6467 return ()

6568 Just input -> H.catch

6669 (do ms <- lift $ processInput input orig mods

@@ -86,6 +89,8 @@ lit f = case splitExtension f of

8689processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])

8790processInput cmd orig inputs

8891 = do i <- getIState

92+ let opts = idris_options i

93+ let quiet = opt_quiet opts

8994 let fn = case inputs of

9095 (f:_) -> f

9196 _ -> ""

@@ -110,7 +115,7 @@ processInput cmd orig inputs

110115 return (Just inputs)

111116 Right Proofs -> do proofs orig

112117 return (Just inputs)

113− Right Quit -> do iputStrLn "Bye bye"

118+ Right Quit -> do when (not quiet) (iputStrLn "Bye bye")

114119 return Nothing

115120 Right cmd -> do idrisCatch (process fn cmd)

116121 (\e -> iputStrLn (show e))

@@ -436,6 +441,7 @@ parseTarget _ = error "unknown target" -- FIXME: partial function

436441

437442parseArgs :: [String] -> [Opt]

438443parseArgs [] = []

444+parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

439445parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

440446parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

441447parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

@@ -487,6 +493,7 @@ idris opts = execStateT (idrisMain opts) idrisInit

487493idrisMain :: [Opt] -> Idris ()

488494idrisMain opts =

489495 do let inputs = opt getFile opts

496+ let quiet = Quiet `elem` opts

490497 let runrepl = not (NoREPL `elem` opts)

491498 let output = opt getOutput opts

492499 let newoutput = opt getNewOutput opts

@@ -504,6 +511,7 @@ idrisMain opts =

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

505512 putIState (i { default_total = True })

506513 setREPL runrepl

514+ setQuiet quiet

507515 setVerbose runrepl

508516 setCmdLine opts

509517 setOutputTy outty

@@ -527,7 +535,7 @@ idrisMain opts =

527535 elabPrims

528536 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

529537 return ()

530− when runrepl $ iputStrLn banner

538+ when (runrepl && not quiet) $ iputStrLn banner

531539 ist <- getIState

532540 mods <- mapM loadModule inputs

533541 ok <- noErrors

src/Main.hs+1

@@ -78,6 +78,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

7878 "--------------" ++ map (\x -> '-') ver ++ "\n" ++

7979 "Usage: idris [input file] [options]\n" ++

8080 "Options:\n" ++

81+ "\t--quiet Quiet mode (for editors)\n" ++

8182 "\t--check Type check only\n" ++

8283 "\t-o [file] Specify output filename\n" ++

8384 "\t-i [dir] Add directory to the list of import paths\n" ++