Permalink
Browse files

quiet mode: for editors

  • Loading branch information...
1 parent 9f1141e commit 228ffdb3df0b7399de4e9ddd1fa6c75dd0ec2752 @raichoo raichoo committed Mar 20, 2013
Showing with 33 additions and 16 deletions.
  1. +6 −0 src/Idris/AbsSyntax.hs
  2. +13 −11 src/Idris/AbsSyntaxTree.hs
  3. +13 −5 src/Idris/REPL.hs
  4. +1 −0 src/Main.hs
View
@@ -279,6 +279,12 @@ setREPL t = do i <- getIState
let opt' = opts { opt_repl = t }
putIState $ i { idris_options = opt' }
+setQuiet :: Bool -> Idris ()
+setQuiet q = do i <- getIState
+ let opts = idris_options i
+ let opt' = opts { opt_quiet = q }
+ putIState $ i { idris_options = opt' }
+
setTarget :: Target -> Idris ()
setTarget t = do i <- getIState
let opts = idris_options i
View
@@ -23,23 +23,24 @@ import Data.Either
import Debug.Trace
-data IOption = IOption { opt_logLevel :: Int,
- opt_typecase :: Bool,
+data IOption = IOption { opt_logLevel :: Int,
+ opt_typecase :: Bool,
opt_typeintype :: Bool,
- opt_coverage :: Bool,
- opt_showimp :: Bool,
+ opt_coverage :: Bool,
+ opt_showimp :: Bool,
opt_errContext :: Bool,
- opt_repl :: Bool,
- opt_verbose :: Bool,
- opt_target :: Target,
- opt_outputTy :: OutputType,
- opt_ibcsubdir :: FilePath,
+ opt_repl :: Bool,
+ opt_verbose :: Bool,
+ opt_quiet :: Bool,
+ opt_target :: Target,
+ opt_outputTy :: OutputType,
+ opt_ibcsubdir :: FilePath,
opt_importdirs :: [FilePath],
- opt_cmdline :: [Opt] -- remember whole command line
+ opt_cmdline :: [Opt] -- remember whole command line
}
deriving (Show, Eq)
-defaultOpts = IOption 0 False False True False False True True ViaC Executable "" [] []
+defaultOpts = IOption 0 False False True False False True True False ViaC Executable "" [] []
-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
-- without typechecking).
@@ -190,6 +191,7 @@ data Command = Quit
data Opt = Filename String
| Ver
| Usage
+ | Quiet
| ShowLibs
| ShowLibdir
| ShowIncs
View
@@ -57,10 +57,13 @@ repl :: IState -- ^ The initial state
-> InputT Idris ()
repl orig mods
= H.catch
- (do let prompt = mkPrompt mods
- x <- getInputLine (prompt ++ "> ")
+ (do let quiet = opt_quiet (idris_options orig)
+ let prompt = if quiet
+ then ""
+ else mkPrompt mods ++ "> "
+ x <- getInputLine prompt
case x of
- Nothing -> do lift $ iputStrLn "Bye bye"
+ Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
return ()
Just input -> H.catch
(do ms <- lift $ processInput input orig mods
@@ -86,6 +89,8 @@ lit f = case splitExtension f of
processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])
processInput cmd orig inputs
= do i <- getIState
+ let opts = idris_options i
+ let quiet = opt_quiet opts
let fn = case inputs of
(f:_) -> f
_ -> ""
@@ -110,7 +115,7 @@ processInput cmd orig inputs
return (Just inputs)
Right Proofs -> do proofs orig
return (Just inputs)
- Right Quit -> do iputStrLn "Bye bye"
+ Right Quit -> do when (not quiet) (iputStrLn "Bye bye")
return Nothing
Right cmd -> do idrisCatch (process fn cmd)
(\e -> iputStrLn (show e))
@@ -436,6 +441,7 @@ parseTarget _ = error "unknown target" -- FIXME: partial function
parseArgs :: [String] -> [Opt]
parseArgs [] = []
+parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
@@ -487,6 +493,7 @@ idris opts = execStateT (idrisMain opts) idrisInit
idrisMain :: [Opt] -> Idris ()
idrisMain opts =
do let inputs = opt getFile opts
+ let quiet = Quiet `elem` opts
let runrepl = not (NoREPL `elem` opts)
let output = opt getOutput opts
let newoutput = opt getNewOutput opts
@@ -504,6 +511,7 @@ idrisMain opts =
when (DefaultTotal `elem` opts) $ do i <- getIState
putIState (i { default_total = True })
setREPL runrepl
+ setQuiet quiet
setVerbose runrepl
setCmdLine opts
setOutputTy outty
@@ -527,7 +535,7 @@ idrisMain opts =
elabPrims
when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
return ()
- when runrepl $ iputStrLn banner
+ when (runrepl && not quiet) $ iputStrLn banner
ist <- getIState
mods <- mapM loadModule inputs
ok <- noErrors
View
@@ -78,6 +78,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++
"--------------" ++ map (\x -> '-') ver ++ "\n" ++
"Usage: idris [input file] [options]\n" ++
"Options:\n" ++
+ "\t--quiet Quiet mode (for editors)\n" ++
"\t--check Type check only\n" ++
"\t-o [file] Specify output filename\n" ++
"\t-i [dir] Add directory to the list of import paths\n" ++

0 comments on commit 228ffdb

Please sign in to comment.