ffc8dc6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #251 from raichoo/master

ffc8dc6Edwin Brady14 years ago

src/Idris/AbsSyntax.hs+6

compare with master

unifiedsplit

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

279 let opt' = opts { opt_repl = t }

280 putIState $ i { idris_options = opt' }

281

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+

282setTarget :: Target -> Idris ()

288setTarget :: Target -> Idris ()

283setTarget t = do i <- getIState

289setTarget t = do i <- getIState

284 let opts = idris_options i

290 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+13−11

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

24import Debug.Trace

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

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

27− opt_typecase :: Bool,

27+ opt_typecase :: Bool,

28 opt_typeintype :: Bool,

29− opt_coverage :: Bool,

29+ opt_coverage :: Bool,

30− opt_showimp :: Bool,

30+ opt_showimp :: Bool,

31 opt_errContext :: Bool,

32− opt_repl :: Bool,

32+ opt_repl :: Bool,

33− opt_verbose :: Bool,

33+ opt_verbose :: Bool,

34+ opt_quiet :: Bool,

34− opt_target :: Target,

35+ opt_target :: Target,

35− opt_outputTy :: OutputType,

36+ opt_outputTy :: OutputType,

36− opt_ibcsubdir :: FilePath,

37+ opt_ibcsubdir :: FilePath,

37 opt_importdirs :: [FilePath],

38 opt_importdirs :: [FilePath],

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

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

39 }

40 }

40 deriving (Show, Eq)

41 deriving (Show, Eq)

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 "" [] []

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

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

45-- without typechecking).

46-- without typechecking).

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

190data Opt = Filename String

191data Opt = Filename String

191 | Ver

192 | Ver

192 | Usage

193 | Usage

194+ | Quiet

193 | ShowLibs

195 | ShowLibs

194 | ShowLibdir

196 | ShowLibdir

195 | ShowIncs

197 | ShowIncs

src/Idris/REPL.hs+13−5

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

57 -> InputT Idris ()

58repl orig mods

59 = H.catch

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

61+ let prompt = if quiet

62+ then ""

60− (do let prompt = mkPrompt mods

63+ else mkPrompt mods ++ "> "

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

64+ x <- getInputLine prompt

62 case x of

65 case x of

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

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

64 return ()

67 return ()

65 Just input -> H.catch

68 Just input -> H.catch

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

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

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

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

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

87processInput cmd orig inputs

90processInput cmd orig inputs

88 = do i <- getIState

91 = do i <- getIState

92+ let opts = idris_options i

93+ let quiet = opt_quiet opts

89 let fn = case inputs of

94 let fn = case inputs of

90 (f:_) -> f

95 (f:_) -> f

91 _ -> ""

96 _ -> ""

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

110 return (Just inputs)

115 return (Just inputs)

111 Right Proofs -> do proofs orig

116 Right Proofs -> do proofs orig

112 return (Just inputs)

117 return (Just inputs)

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

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

114 return Nothing

119 return Nothing

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

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

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

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

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

436

441

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

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

438parseArgs [] = []

443parseArgs [] = []

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

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

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

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

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

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

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

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

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

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

488idrisMain opts =

494idrisMain opts =

489 do let inputs = opt getFile opts

495 do let inputs = opt getFile opts

496+ let quiet = Quiet `elem` opts

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

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

491 let output = opt getOutput opts

498 let output = opt getOutput opts

492 let newoutput = opt getNewOutput opts

499 let newoutput = opt getNewOutput opts

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

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

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

505 putIState (i { default_total = True })

512 putIState (i { default_total = True })

506 setREPL runrepl

513 setREPL runrepl

514+ setQuiet quiet

507 setVerbose runrepl

515 setVerbose runrepl

508 setCmdLine opts

516 setCmdLine opts

509 setOutputTy outty

517 setOutputTy outty

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

527 elabPrims

535 elabPrims

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

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

529 return ()

537 return ()

530− when runrepl $ iputStrLn banner

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

531 ist <- getIState

539 ist <- getIState

532 mods <- mapM loadModule inputs

540 mods <- mapM loadModule inputs

533 ok <- noErrors

541 ok <- noErrors

src/Main.hs+1

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

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

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

80 "Options:\n" ++

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

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

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

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

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

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

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