git.iko.soy/Idris-dev
on master help sign in
Banner
commit796fa2536847bda023bb1d2b28425b68f9362a74 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 23 Oct 2011, 22:36 (15 years ago) parent5f7eed8
3 files changed+27−8
compare with master
unifiedsplit
src/Idris/Parser.hs+3−1 src/Idris/REPL.hs+5−4 src/Main.hs+19−3
src/Idris/Parser.hs+3−1
@@ -45,7 +45,7 @@ lchar = lexeme.char
4545
4646-- Loading modules
4747
48−loadModule :: FilePath -> Idris ()
48+loadModule :: FilePath -> Idris String
4949loadModule f = do datadir <- lift $ getDataDir
5050 fp <- lift $ findImport [".", datadir] f
5151 i <- getIState
@@ -55,6 +55,8 @@ loadModule f = do datadir <- lift $ getDataDir
5555 case fp of
5656 IDR fn -> loadSource fn
5757 IBC fn -> error "Not implemented"
58+ let (dir, fh) = splitFileName f
59+ return (dropExtension fh)
5860
5961loadSource :: FilePath -> Idris ()
6062loadSource f = do iLOG ("Reading " ++ f)
src/Idris/REPL.hs+5−4
@@ -18,13 +18,14 @@ import Control.Monad
1818import Control.Monad.State
1919import Data.List
2020
21−repl :: Idris ()
22−repl = do x <- lift $ readline "Idris> "
21+repl :: String -> Idris ()
22+repl prompt
23+ = do x <- lift $ readline (prompt ++ "> ")
2324 case x of
24− Nothing -> repl
25+ Nothing -> repl prompt
2526 Just input -> do lift $ addHistory input
2627 continue <- processInput input
27− when continue repl
28+ when continue (repl prompt)
2829
2930processInput :: String -> Idris Bool
3031processInput cmd
src/Main.hs+19−3
@@ -6,6 +6,7 @@ import System.Environment
66import System.Exit
77
88import Data.Maybe
9+import Data.Version
910import Control.Monad.State
1011
1112import Core.CoreParser
@@ -21,6 +22,7 @@ import Idris.REPL
2122import Idris.ElabDecls
2223import Idris.Primitives
2324import Idris.Imports
25+import Paths_miniidris
2426
2527-- Main program reads command line options, parses the main program, and gets
2628-- on with the REPL.
@@ -41,13 +43,19 @@ runIdris opts =
4143 do let inputs = opt getFile opts
4244 mapM_ makeOption opts
4345 elabPrims
44− when (not (NoPrelude `elem` opts)) $ loadModule "prelude"
45− mapM_ loadModule inputs
46− when (not (NoREPL `elem` opts)) $ repl
46+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
47+ return ()
48+ mods <- mapM loadModule inputs
49+ when (not (NoREPL `elem` opts)) $ do iputStrLn banner
50+ repl (mkPrompt mods)
4751 where
4852 makeOption (OLogging i) = setLogLevel i
4953 makeOption _ = return ()
5054
55+mkPrompt [] = "Idris"
56+mkPrompt [x] = "*" ++ x
57+mkPrompt (x:xs) = "*" ++ x ++ " " ++ mkPrompt xs
58+
5159getFile :: Opt -> Maybe String
5260getFile (Filename str) = Just str
5361getFile _ = Nothing
@@ -79,3 +87,11 @@ main'
7987 err -> print err
8088 -}
8189
90+ver = showVersion version
91+
92+banner = " ____ __ _ \n" ++
93+ " / _/___/ /____(_)____ \n" ++
94+ " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
95+ " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
96+ " /___/\\__,_/_/ /_/____/ Type :? for help \n"
97+