b5eee09 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Convert IO errors into erros in the Idris monad

Introduces a variant of liftIO, called runIO, that converts IO errors into Idris errors with the Msg constructor. Fixes #543.

commitb5eee0918bec5c5f2d81af0918985229acc76014 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 18 Oct 2013, 10:36 (13 years ago) parenta9f184d

8 files changed+99−93

compare with master

unifiedsplit

src/IRTS/Compiler.hs+17−18 src/Idris/AbsSyntax.hs+21−13 src/Idris/Chaser.hs+13−13 src/Idris/IBC.hs+7−7 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+31−31 src/Main.hs+8−9

src/IRTS/Compiler.hs+17−18

@@ -67,31 +67,30 @@ compile codegen f tm

6767 dumpDefun <- getDumpDefun

6868 case dumpCases of

6969 Nothing -> return ()

70− Just f -> liftIO $ writeFile f (showCaseTrees tagged)

70+ Just f -> runIO $ writeFile f (showCaseTrees tagged)

7171 case dumpDefun of

7272 Nothing -> return ()

73− Just f -> liftIO $ writeFile f (dumpDefuns defuns)

73+ Just f -> runIO $ writeFile f (dumpDefuns defuns)

7474 triple <- targetTriple

7575 cpu <- targetCPU

7676 optimize <- optLevel

7777 iLOG "Building output"

7878 case checked of

79− OK c -> liftIO $ case codegen of

80− ViaC ->

81− codegenC c f outty hdrs

82− (concatMap mkObj objs)

83− (concatMap mkLib libs)

84− (concatMap mkFlag flags ++

85− concatMap incdir impdirs) NONE

86− ViaJava ->

87− codegenJava [] c f hdrs libs outty

88− ViaJavaScript ->

89− codegenJavaScript JavaScript c f outty

90− ViaNode ->

91− codegenJavaScript Node c f outty

92− ViaLLVM -> codegenLLVM c triple cpu optimize f outty

93−

94− Bytecode -> dumpBC c f

79+ OK c -> runIO $ case codegen of

80+ ViaC ->

81+ codegenC c f outty hdrs

82+ (concatMap mkObj objs)

83+ (concatMap mkLib libs)

84+ (concatMap mkFlag flags ++

85+ concatMap incdir impdirs) NONE

86+ ViaJava ->

87+ codegenJava [] c f hdrs libs outty

88+ ViaJavaScript ->

89+ codegenJavaScript JavaScript c f outty

90+ ViaNode ->

91+ codegenJavaScript Node c f outty

92+ ViaLLVM -> codegenLLVM c triple cpu optimize f outty

93+ Bytecode -> dumpBC c f

9594 Error e -> ierror e

9695 where checkMVs = do i <- getIState

9796 case idris_metavars i \\ primDefs of

src/Idris/AbsSyntax.hs+21−13

@@ -27,6 +27,9 @@ import Data.Word (Word)

2727

2828import Debug.Trace

2929

30+import Control.Monad.Error (throwError, catchError)

31+import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)

32+

3033import Util.Pretty

3134import Util.System

3235

@@ -221,6 +224,11 @@ getIState = get

221224putIState :: IState -> Idris ()

222225putIState = put

223226

227+-- | A version of liftIO that puts errors into the exception type of the Idris monad

228+runIO :: IO a -> Idris a

229+runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return

230+-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"

231+

224232getName :: Idris Int

225233getName = do i <- getIState;

226234 let idx = idris_name i;

@@ -282,25 +290,25 @@ iPrintResult s = do i <- getIState

282290 case idris_outputmode i of

283291 RawOutput -> case s of

284292 "" -> return ()

285− s -> liftIO $ putStrLn s

293+ s -> runIO $ putStrLn s

286294 IdeSlave n ->

287295 let good = SexpList [SymbolAtom "ok", toSExp s] in

288− liftIO $ putStrLn $ convSExp "return" good n

296+ runIO $ putStrLn $ convSExp "return" good n

289297

290298iPrintError :: String -> Idris ()

291299iPrintError s = do i <- getIState

292300 case idris_outputmode i of

293301 RawOutput -> case s of

294302 "" -> return ()

295− s -> liftIO $ putStrLn s

303+ s -> runIO $ putStrLn s

296304 IdeSlave n ->

297305 let good = SexpList [SymbolAtom "error", toSExp s] in

298− liftIO . putStrLn $ convSExp "return" good n

306+ runIO . putStrLn $ convSExp "return" good n

299307

300308iputStrLn :: String -> Idris ()

301309iputStrLn s = do i <- getIState

302310 case idris_outputmode i of

303− RawOutput -> liftIO $ putStrLn s

311+ RawOutput -> runIO $ putStrLn s

304312 IdeSlave n ->

305313 case span (/=':') s of

306314 (fn, ':':rest) -> case span isDigit rest of

@@ -308,31 +316,31 @@ iputStrLn s = do i <- getIState

308316 ([], msg) -> write

309317 (num, ':':msg) -> iWarn (FC fn (read num)) msg

310318 _ -> write

311− where write = liftIO . putStrLn $ convSExp "write-string" s n

319+ where write = runIO . putStrLn $ convSExp "write-string" s n

312320

313321ideslavePutSExp :: SExpable a => String -> a -> Idris ()

314322ideslavePutSExp cmd info = do i <- getIState

315323 case idris_outputmode i of

316− IdeSlave n -> liftIO . putStrLn $ convSExp cmd info n

324+ IdeSlave n -> runIO . putStrLn $ convSExp cmd info n

317325 _ -> return ()

318326

319327-- this needs some typing magic and more structured output towards emacs

320328iputGoal :: String -> Idris ()

321329iputGoal s = do i <- getIState

322330 case idris_outputmode i of

323− RawOutput -> liftIO $ putStrLn s

324− IdeSlave n -> liftIO . putStrLn $ convSExp "write-goal" s n

331+ RawOutput -> runIO $ putStrLn s

332+ IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n

325333

326334isetPrompt :: String -> Idris ()

327335isetPrompt p = do i <- getIState

328336 case idris_outputmode i of

329− IdeSlave n -> liftIO . putStrLn $ convSExp "set-prompt" p n

337+ IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

330338

331339iWarn :: FC -> String -> Idris ()

332340iWarn fc err = do i <- getIState

333341 case idris_outputmode i of

334− RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)

335− IdeSlave n -> liftIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

342+ RawOutput -> runIO $ putStrLn (show fc ++ ":" ++ err)

343+ IdeSlave n -> runIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

336344

337345setLogLevel :: Int -> Idris ()

338346setLogLevel l = do i <- getIState

@@ -543,7 +551,7 @@ logLvl :: Int -> String -> Idris ()

543551logLvl l str = do i <- getIState

544552 let lvl = opt_logLevel (idris_options i)

545553 when (lvl >= l)

546− $ do liftIO (putStrLn str)

554+ $ do runIO (putStrLn str)

547555 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }

548556

549557cmdOptType :: Opt -> Idris Bool

src/Idris/Chaser.hs+13−13

@@ -71,7 +71,7 @@ getIModTime (LIDR i) = getModificationTime i

7171buildTree :: [FilePath] -> -- already guaranteed built

7272 FilePath -> Idris [ModuleTree]

7373buildTree built fp = idrisCatch (btree [] fp)

74− (\e -> do now <- liftIO $ getCurrentTime

74+ (\e -> do now <- runIO $ getCurrentTime

7575 return [MTree (IDR fp) True now []])

7676 where

7777 btree done f =

@@ -80,8 +80,8 @@ buildTree built fp = idrisCatch (btree [] fp)

8080 iLOG $ "CHASING " ++ show file

8181 ibcsd <- valIBCSubDir i

8282 ids <- allImportDirs

83− fp <- liftIO $ findImport ids ibcsd file

84− mt <- liftIO $ getIModTime fp

83+ fp <- runIO $ findImport ids ibcsd file

84+ mt <- runIO $ getIModTime fp

8585 if (file `elem` built)

8686 then return [MTree fp False mt []]

8787 else if file `elem` done

@@ -89,19 +89,19 @@ buildTree built fp = idrisCatch (btree [] fp)

8989 else mkChildren fp

9090

9191 where mkChildren (LIDR fn) = do ms <- children True fn (f:done)

92− mt <- liftIO $ getModificationTime fn

92+ mt <- runIO $ getModificationTime fn

9393 return [MTree (LIDR fn) True mt ms]

9494 mkChildren (IDR fn) = do ms <- children False fn (f:done)

95− mt <- liftIO $ getModificationTime fn

95+ mt <- runIO $ getModificationTime fn

9696 return [MTree (IDR fn) True mt ms]

9797 mkChildren (IBC fn src)

98− = do srcexist <- liftIO $ doesFileExist (getSrcFile src)

98+ = do srcexist <- runIO $ doesFileExist (getSrcFile src)

9999 ms <- if srcexist then

100100 do [MTree _ _ _ ms'] <- mkChildren src

101101 return ms'

102102 else return []

103− mt <- idrisCatch (liftIO $ getModificationTime fn)

104− (\c -> liftIO $ getIModTime src)

103+ mt <- idrisCatch (runIO $ getModificationTime fn)

104+ (\c -> runIO $ getIModTime src)

105105 ok <- checkIBCUpToDate fn src

106106 return [MTree (IBC fn src) ok mt ms]

107107

@@ -115,18 +115,18 @@ buildTree built fp = idrisCatch (btree [] fp)

115115 checkIBCUpToDate fn (LIDR src) = older fn src

116116 checkIBCUpToDate fn (IDR src) = older fn src

117117

118− older ibc src = do exist <- liftIO $ doesFileExist src

118+ older ibc src = do exist <- runIO $ doesFileExist src

119119 if exist then do

120− ibct <- liftIO $ getModificationTime ibc

121− srct <- liftIO $ getModificationTime src

120+ ibct <- runIO $ getModificationTime ibc

121+ srct <- runIO $ getModificationTime src

122122 return (srct > ibct)

123123 else return False

124124

125125 children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]

126126 children lit f done = idrisCatch

127− (do exist <- liftIO $ doesFileExist f

127+ (do exist <- runIO $ doesFileExist f

128128 if exist then do

129− file_in <- liftIO $ readFile f

129+ file_in <- runIO $ readFile f

130130 file <- if lit then tclift $ unlit f file_in else return file_in

131131 (_, modules, _) <- parseImports f file

132132 ms <- mapM (btree done) modules

src/Idris/IBC.hs+7−7

@@ -62,7 +62,7 @@ initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

6262

6363loadIBC :: FilePath -> Idris ()

6464loadIBC fp = do iLOG $ "Loading ibc " ++ fp

65− ibcf <- liftIO $ (decodeFile fp :: IO IBCFile)

65+ ibcf <- runIO $ (decodeFile fp :: IO IBCFile)

6666 process ibcf fp

6767

6868writeIBC :: FilePath -> FilePath -> Idris ()

@@ -73,8 +73,8 @@ writeIBC src f

7373 (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

7474 [] -> return ()

7575 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

76− idrisCatch (do liftIO $ createDirectoryIfMissing True (dropFileName f)

77− liftIO $ encodeFile f ibcf

76+ idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

77+ runIO $ encodeFile f ibcf

7878 iLOG "Written")

7979 (\c -> do iLOG $ "Failed " ++ show c)

8080 return ()

@@ -140,8 +140,8 @@ process i fn

140140 | ver i /= ibcVersion = do iLOG "ibc out of date"

141141 ifail "Incorrect ibc version --- please rebuild"

142142 | otherwise =

143− do srcok <- liftIO $ doesFileExist (sourcefile i)

144− when srcok $ liftIO $ timestampOlder (sourcefile i) fn

143+ do srcok <- runIO $ doesFileExist (sourcefile i)

144+ when srcok $ runIO $ timestampOlder (sourcefile i) fn

145145 v <- verbose

146146 quiet <- getQuiet

147147-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i

@@ -181,7 +181,7 @@ pImports fs

181181 = do mapM_ (\f -> do i <- getIState

182182 ibcsd <- valIBCSubDir i

183183 ids <- allImportDirs

184− fp <- liftIO $ findImport ids ibcsd f

184+ fp <- runIO $ findImport ids ibcsd f

185185 if (f `elem` imported i)

186186 then iLOG $ "Already read " ++ f

187187 else do putIState (i { imported = f : imported i })

@@ -259,7 +259,7 @@ pKeywords k = do i <- getIState

259259

260260pObjs :: [(Codegen, FilePath)] -> Idris ()

261261pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs

262− o <- liftIO $ findInPath dirs obj

262+ o <- runIO $ findInPath dirs obj

263263 addObjectFile cg o) os

264264

265265pLibs :: [(Codegen, String)] -> Idris ()

src/Idris/Parser.hs+1−1

@@ -975,7 +975,7 @@ loadSource lidr f

975975 = do iLOG ("Reading " ++ f)

976976 i <- getIState

977977 let def_total = default_total i

978− file_in <- liftIO $ readFile f

978+ file_in <- runIO $ readFile f

979979 file <- if lidr then tclift $ unlit f file_in else return file_in

980980 (mname, modules, pos) <- parseImports f file

981981 i <- getIState

src/Idris/Prover.hs+1−1

@@ -136,7 +136,7 @@ lifte st e = do (v, _) <- elabStep st e

136136receiveInput :: ElabState [PDecl] -> Idris (Maybe String)

137137receiveInput e =

138138 do i <- getIState

139− l <- liftIO $ getLine

139+ l <- runIO $ getLine

140140 let (sexp, id) = parseMessage l

141141 putIState $ i { idris_outputmode = (IdeSlave id) }

142142 case sexpToCommand sexp of

src/Idris/REPL.hs+31−31

@@ -58,7 +58,7 @@ import System.IO

5858import Control.Monad

5959import Control.Monad.Trans.Error (ErrorT(..))

6060import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )

61−import Control.Monad.Trans ( liftIO, lift )

61+import Control.Monad.Trans ( lift )

6262import Data.Maybe

6363import Data.List

6464import Data.Char

@@ -111,7 +111,7 @@ ideslaveStart orig mods

111111ideslave :: IState -> [FilePath] -> Idris ()

112112ideslave orig mods

113113 = do idrisCatch

114− (do l <- liftIO $ getLine

114+ (do l <- runIO $ getLine

115115 let (sexp, id) = parseMessage l

116116 i <- getIState

117117 putIState $ i { idris_outputmode = (IdeSlave id) }

@@ -134,7 +134,7 @@ ideslave orig mods

134134 Just (REPLCompletions str) ->

135135 do (unused, compls) <- replCompletion (reverse str, "")

136136 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]

137− liftIO $ putStrLn $ convSExp "return" good id

137+ runIO $ putStrLn $ convSExp "return" good id

138138 Just (LoadFile filename) ->

139139 do clearErr

140140 putIState (orig { idris_options = idris_options i,

@@ -224,7 +224,7 @@ processInput cmd orig inputs

224224 _ -> ""

225225 c <- colourise

226226 case parseCmd i "(input)" cmd of

227− Failure err -> do liftIO $ print (fixColour c err)

227+ Failure err -> do runIO $ print (fixColour c err)

228228 return (Just inputs)

229229 Success Reload ->

230230 do putIState $ orig { idris_options = idris_options i

@@ -275,13 +275,13 @@ edit :: FilePath -> IState -> Idris ()

275275edit "" orig = iputStrLn "Nothing to edit"

276276edit f orig

277277 = do i <- getIState

278− env <- liftIO $ getEnvironment

278+ env <- runIO $ getEnvironment

279279 let editor = getEditor env

280280 let line = case errLine i of

281281 Just l -> " +" ++ show l ++ " "

282282 Nothing -> " "

283283 let cmd = editor ++ line ++ f

284− liftIO $ system cmd

284+ runIO $ system cmd

285285 clearErr

286286 putIState $ orig { idris_options = idris_options i

287287 , idris_colourTheme = idris_colourTheme i

@@ -311,7 +311,7 @@ insertScript prf (x : xs) = x : insertScript prf xs

311311process :: FilePath -> Command -> Idris ()

312312process fn Help = iPrintResult displayHelp

313313process fn (ChangeDirectory f)

314− = do liftIO $ setCurrentDirectory f

314+ = do runIO $ setCurrentDirectory f

315315 return ()

316316process fn (Eval t)

317317 = do (tm, ty) <- elabVal toplevel False t

@@ -443,17 +443,17 @@ process fn (RmProof n')

443443

444444process fn' (AddProof prf)

445445 = do fn <- do

446− ex <- liftIO $ doesFileExist fn'

446+ ex <- runIO $ doesFileExist fn'

447447 let fnExt = fn' <.> "idr"

448− exExt <- liftIO $ doesFileExist fnExt

448+ exExt <- runIO $ doesFileExist fnExt

449449 if ex

450450 then return fn'

451451 else if exExt

452452 then return fnExt

453453 else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"

454454 let fb = fn ++ "~"

455− liftIO $ copyFile fn fb -- make a backup in case something goes wrong!

456− prog <- liftIO $ readFile fb

455+ runIO $ copyFile fn fb -- make a backup in case something goes wrong!

456+ prog <- runIO $ readFile fb

457457 i <- getIState

458458 let proofs = proof_list i

459459 n' <- case prf of

@@ -465,7 +465,7 @@ process fn' (AddProof prf)

465465 case lookup n proofs of

466466 Nothing -> iputStrLn "No proof to add"

467467 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls

468− liftIO $ writeFile fn (unlines prog')

468+ runIO $ writeFile fn (unlines prog')

469469 removeProof n

470470 iputStrLn $ "Added proof " ++ show n

471471 where ls = (lines prog)

@@ -513,11 +513,11 @@ process fn Execute = do (m, _) <- elabVal toplevel False

513513 (PRef fc (UN "run__IO"))

514514 [pexp $ PRef fc (NS (UN "main") ["Main"])])

515515-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

516− (tmpn, tmph) <- liftIO tempfile

517− liftIO $ hClose tmph

516+ (tmpn, tmph) <- runIO tempfile

517+ runIO $ hClose tmph

518518 t <- codegen

519519 compile t tmpn m

520− liftIO $ system tmpn

520+ runIO $ system tmpn

521521 return ()

522522 where fc = FC "main" 0

523523process fn (Compile codegen f)

@@ -774,10 +774,10 @@ idrisMain opts =

774774 [] -> 2

775775 xs -> last xs

776776 trpl <- case opt getTriple opts of

777− [] -> liftIO $ getDefaultTargetTriple

777+ [] -> runIO $ getDefaultTargetTriple

778778 xs -> return (last xs)

779779 tcpu <- case opt getCPU opts of

780− [] -> liftIO $ getHostCPUName

780+ [] -> runIO $ getHostCPUName

781781 xs -> return (last xs)

782782 let outty = case opt getOutputTy opts of

783783 [] -> Executable

@@ -788,7 +788,7 @@ idrisMain opts =

788788 script <- case opt getExecScript opts of

789789 [] -> return Nothing

790790 x:y:xs -> do iputStrLn "More than one interpreter expression found."

791− liftIO $ exitWith (ExitFailure 1)

791+ runIO $ exitWith (ExitFailure 1)

792792 [expr] -> return (Just expr)

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

794794 putIState (i { default_total = True })

@@ -809,11 +809,11 @@ idrisMain opts =

809809 -- if we have the --fovm flag, drop into the first order VM testing

810810 case vm of

811811 [] -> return ()

812− xs -> liftIO $ mapM_ (fovm cgn outty) xs

812+ xs -> runIO $ mapM_ (fovm cgn outty) xs

813813 -- if we have the --bytecode flag, drop into the bytecode assembler

814814 case bcs of

815815 [] -> return ()

816− xs -> return () -- liftIO $ mapM_ bcAsm xs

816+ xs -> return () -- runIO $ mapM_ bcAsm xs

817817 case ibcsubdir of

818818 [] -> setIBCSubDir ""

819819 (d:_) -> setIBCSubDir d

@@ -829,7 +829,7 @@ idrisMain opts =

829829

830830 loadInputs inputs

831831

832− liftIO $ hSetBuffering stdout LineBuffering

832+ runIO $ hSetBuffering stdout LineBuffering

833833

834834 ok <- noErrors

835835 when ok $ case output of

@@ -845,7 +845,7 @@ idrisMain opts =

845845 when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist inputs

846846 when (idesl) $ ideslaveStart ist inputs

847847 ok <- noErrors

848− when (not ok) $ liftIO (exitWith (ExitFailure 1))

848+ when (not ok) $ runIO (exitWith (ExitFailure 1))

849849 where

850850 makeOption (OLogging i) = setLogLevel i

851851 makeOption TypeCase = setTypeCase True

@@ -855,7 +855,7 @@ idrisMain opts =

855855 makeOption _ = return ()

856856

857857 addPkgDir :: String -> Idris ()

858− addPkgDir p = do ddir <- liftIO $ getDataDir

858+ addPkgDir p = do ddir <- runIO $ getDataDir

859859 addImportDir (ddir </> p)

860860

861861execScript :: String -> Idris ()

@@ -863,11 +863,11 @@ execScript expr = do i <- getIState

863863 c <- colourise

864864 case parseExpr i expr of

865865 Failure err -> do iputStrLn $ show (fixColour c err)

866− liftIO $ exitWith (ExitFailure 1)

866+ runIO $ exitWith (ExitFailure 1)

867867 Success term -> do ctxt <- getContext

868868 (tm, _) <- elabVal toplevel False term

869869 res <- execute tm

870− liftIO $ exitWith ExitSuccess

870+ runIO $ exitWith ExitSuccess

871871

872872-- | Check if the coloring matches the options and corrects if necessary

873873fixColour :: Bool -> ANSI.Doc -> ANSI.Doc

@@ -876,7 +876,7 @@ fixColour True doc = doc

876876

877877-- | Get the platform-specific, user-specific Idris dir

878878getIdrisUserDataDir :: Idris FilePath

879−getIdrisUserDataDir = liftIO $ getAppUserDataDirectory "idris"

879+getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"

880880

881881-- | Locate the platform-specific location for the init script

882882getInitScript :: Idris FilePath

@@ -886,24 +886,24 @@ getInitScript = do idrisDir <- getIdrisUserDataDir

886886-- | Run the initialisation script

887887initScript :: Idris ()

888888initScript = do script <- getInitScript

889− idrisCatch (do go <- liftIO $ doesFileExist script

889+ idrisCatch (do go <- runIO $ doesFileExist script

890890 when go $ do

891− h <- liftIO $ openFile script ReadMode

891+ h <- runIO $ openFile script ReadMode

892892 runInit h

893− liftIO $ hClose h)

893+ runIO $ hClose h)

894894 (\e -> iPrintError $ "Error reading init file: " ++ show e)

895895 where runInit :: Handle -> Idris ()

896896 runInit h = do eof <- lift . lift $ hIsEOF h

897897 ist <- getIState

898898 unless eof $ do

899− line <- liftIO $ hGetLine h

899+ line <- runIO $ hGetLine h

900900 script <- getInitScript

901901 c <- colourise

902902 processLine ist line script c

903903 runInit h

904904 processLine i cmd input clr =

905905 case parseCmd i input cmd of

906− Failure err -> liftIO $ print (fixColour clr err)

906+ Failure err -> runIO $ print (fixColour clr err)

907907 Success Reload -> iPrintError "Init scripts cannot reload the file"

908908 Success (Load f) -> iPrintError "Init scripts cannot load files"

909909 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"

src/Main.hs+8−9

@@ -10,7 +10,6 @@ import Data.Maybe

1010import Data.Version

1111import Control.Monad.Trans.Error ( ErrorT(..) )

1212import Control.Monad.Trans.State.Strict ( execStateT, get, put )

13−import Control.Monad.Trans ( liftIO )

1413import Control.Monad ( when )

1514

1615import Core.CoreParser

@@ -45,18 +44,18 @@ main = do xs <- getArgs

4544

4645runIdris :: [Opt] -> Idris ()

4746runIdris opts = do

48− when (Ver `elem` opts) $ liftIO showver

49− when (Usage `elem` opts) $ liftIO usage

50− when (ShowIncs `elem` opts) $ liftIO showIncs

51− when (ShowLibs `elem` opts) $ liftIO showLibs

52− when (ShowLibdir `elem` opts) $ liftIO showLibdir

47+ when (Ver `elem` opts) $ runIO showver

48+ when (Usage `elem` opts) $ runIO usage

49+ when (ShowIncs `elem` opts) $ runIO showIncs

50+ when (ShowLibs `elem` opts) $ runIO showLibs

51+ when (ShowLibdir `elem` opts) $ runIO showLibdir

5352 case opt getPkgClean opts of

5453 [] -> return ()

55− fs -> do liftIO $ mapM_ cleanPkg fs

56− liftIO $ exitWith ExitSuccess

54+ fs -> do runIO $ mapM_ cleanPkg fs

55+ runIO $ exitWith ExitSuccess

5756 case opt getPkg opts of

5857 [] -> idrisMain opts -- in Idris.REPL

59− fs -> liftIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs

58+ fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs

6059

6160usage = do putStrLn usagemsg

6261 exitWith ExitSuccess