@@ -69,9 +69,10 @@ buildPkg warnonly (install, fp)
6969-- This differs from build in that executables are not built, if the
7070-- package contains an executable.
7171checkPkg :: Bool -- ^ Show Warnings
72+ -> Bool -- ^ quit on failure
7273 -> FilePath -- ^ Path to ipkg file.
7374 -> IO ()
74−checkPkg warnonly fpath
75+checkPkg warnonly quit fpath
7576 = do pkgdesc <-parseDesc fpath
7677 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
7778 when (and ok) $
@@ -81,12 +82,31 @@ checkPkg warnonly fpath
8182 res <- buildMods (NoREPL : Verbose : idris_opts pkgdesc)
8283 (modules pkgdesc)
8384 setCurrentDirectory dir
84− case res of
85− Nothing -> exitWith (ExitFailure 1)
86− Just res' -> do
87− case errLine res' of
88− Just _ -> exitWith (ExitFailure 1)
89− _ -> return ()
85+ when quit $ case res of
86+ Nothing -> exitWith (ExitFailure 1)
87+ Just res' -> do
88+ case errLine res' of
89+ Just _ -> exitWith (ExitFailure 1)
90+ _ -> return ()
91+
92+-- | Check a package and start a REPL
93+replPkg :: FilePath -> Idris ()
94+replPkg fp = do orig <- getIState
95+ runIO $ checkPkg False False fp
96+ pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition!
97+ let opts = idris_opts pkgdesc
98+ let mod = idris_main pkgdesc
99+ let f = toPath (showCG mod)
100+ putIState orig
101+ dir <- runIO $ getCurrentDirectory
102+ runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
103+
104+ if (f /= "")
105+ then idrisMain ((Filename f) : opts)
106+ else iputStrLn "Can't start REPL: no main module given"
107+ runIO $ setCurrentDirectory dir
108+
109+ where toPath n = foldl1' (</>) $ splitOn "." n
90110
91111-- | Clean Package build files
92112cleanPkg :: FilePath -- ^ Path to ipkg file.