git.iko.soy/Idris-dev
on master help sign in
Add --repl [package] command line option
63d2989Edwin Brady
main/Main.hs+5−2
compare with master
unifiedsplit
@@ -55,14 +55,17 @@ runIdris opts = do
55 when (ShowLibdir `elem` opts) $ runIO showLibdir
55 when (ShowLibdir `elem` opts) $ runIO showLibdir
56 case opt getPkgCheck opts of
56 case opt getPkgCheck opts of
57 [] -> return ()
57 [] -> return ()
58− fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts)) fs
58+ fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts) True) fs
59 runIO $ exitWith ExitSuccess
59 runIO $ exitWith ExitSuccess
60 case opt getPkgClean opts of
60 case opt getPkgClean opts of
61 [] -> return ()
61 [] -> return ()
62 fs -> do runIO $ mapM_ cleanPkg fs
62 fs -> do runIO $ mapM_ cleanPkg fs
63 runIO $ exitWith ExitSuccess
63 runIO $ exitWith ExitSuccess
64 case opt getPkg opts of
64 case opt getPkg opts of
65+ [] -> case opt getPkgREPL opts of
65− [] -> idrisMain opts -- in Idris.REPL
66+ [] -> idrisMain opts
67+ [f] -> replPkg f
68+ _ -> ifail "Too many packages"
66 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
69 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
67
70
68usage = do putStrLn usagemsg
71usage = do putStrLn usagemsg
src/Idris/AbsSyntaxTree.hs+1
@@ -315,6 +315,7 @@ data Opt = Filename String
315 | PkgInstall String
315 | PkgInstall String
316 | PkgClean String
316 | PkgClean String
317 | PkgCheck String
317 | PkgCheck String
318+ | PkgREPL String
318 | WarnOnly
319 | WarnOnly
319 | Pkg String
320 | Pkg String
320 | BCAsm String
321 | BCAsm String
src/Idris/REPL.hs+5
@@ -1019,6 +1019,7 @@ parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)
1019parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
1019parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)
1020parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
1020parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)
1021parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
1021parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)
1022+parseArgs ("--repl":n:ns) = PkgREPL n : (parseArgs ns)
1022parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
1023parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)
1023parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)
1024parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)
1024-- Misc Options
1025-- Misc Options
@@ -1336,6 +1337,10 @@ getPkgClean :: Opt -> Maybe String
1336getPkgClean (PkgClean str) = Just str
1337getPkgClean (PkgClean str) = Just str
1337getPkgClean _ = Nothing
1338getPkgClean _ = Nothing
1338
1339
1340+getPkgREPL :: Opt -> Maybe String
1341+getPkgREPL (PkgREPL str) = Just str
1342+getPkgREPL _ = Nothing
1343+
1339getPkgCheck :: Opt -> Maybe String
1344getPkgCheck :: Opt -> Maybe String
1340getPkgCheck (PkgCheck str) = Just str
1345getPkgCheck (PkgCheck str) = Just str
1341getPkgCheck _ = Nothing
1346getPkgCheck _ = Nothing
src/Pkg/Package.hs+27−7
@@ -69,9 +69,10 @@ buildPkg warnonly (install, fp)
69-- This differs from build in that executables are not built, if the
69-- This differs from build in that executables are not built, if the
70-- package contains an executable.
70-- package contains an executable.
71checkPkg :: Bool -- ^ Show Warnings
71checkPkg :: Bool -- ^ Show Warnings
72+ -> Bool -- ^ quit on failure
72 -> FilePath -- ^ Path to ipkg file.
73 -> FilePath -- ^ Path to ipkg file.
73 -> IO ()
74 -> IO ()
74−checkPkg warnonly fpath
75+checkPkg warnonly quit fpath
75 = do pkgdesc <-parseDesc fpath
76 = do pkgdesc <-parseDesc fpath
76 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
77 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)
77 when (and ok) $
78 when (and ok) $
@@ -81,12 +82,31 @@ checkPkg warnonly fpath
81 res <- buildMods (NoREPL : Verbose : idris_opts pkgdesc)
82 res <- buildMods (NoREPL : Verbose : idris_opts pkgdesc)
82 (modules pkgdesc)
83 (modules pkgdesc)
83 setCurrentDirectory dir
84 setCurrentDirectory dir
84− case res of
85+ when quit $ case res of
85− Nothing -> exitWith (ExitFailure 1)
86+ Nothing -> exitWith (ExitFailure 1)
86− Just res' -> do
87+ Just res' -> do
87− case errLine res' of
88+ case errLine res' of
88− Just _ -> exitWith (ExitFailure 1)
89+ Just _ -> exitWith (ExitFailure 1)
89− _ -> return ()
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
90
110
91-- | Clean Package build files
111-- | Clean Package build files
92cleanPkg :: FilePath -- ^ Path to ipkg file.
112cleanPkg :: FilePath -- ^ Path to ipkg file.