git.iko.soy/Idris-dev
on master help sign in
Banner
796fa25Edwin Brady
src/Idris/Parser.hs+3−1
compare with master
unifiedsplit
@@ -45,7 +45,7 @@ lchar = lexeme.char
45
45
46-- Loading modules
46-- Loading modules
47
47
48−loadModule :: FilePath -> Idris ()
48+loadModule :: FilePath -> Idris String
49loadModule f = do datadir <- lift $ getDataDir
49loadModule f = do datadir <- lift $ getDataDir
50 fp <- lift $ findImport [".", datadir] f
50 fp <- lift $ findImport [".", datadir] f
51 i <- getIState
51 i <- getIState
@@ -55,6 +55,8 @@ loadModule f = do datadir <- lift $ getDataDir
55 case fp of
55 case fp of
56 IDR fn -> loadSource fn
56 IDR fn -> loadSource fn
57 IBC fn -> error "Not implemented"
57 IBC fn -> error "Not implemented"
58+ let (dir, fh) = splitFileName f
59+ return (dropExtension fh)
58
60
59loadSource :: FilePath -> Idris ()
61loadSource :: FilePath -> Idris ()
60loadSource f = do iLOG ("Reading " ++ f)
62loadSource f = do iLOG ("Reading " ++ f)
src/Idris/REPL.hs+5−4
@@ -18,13 +18,14 @@ import Control.Monad
18import Control.Monad.State
18import Control.Monad.State
19import Data.List
19import Data.List
20
20
21−repl :: Idris ()
21+repl :: String -> Idris ()
22+repl prompt
22−repl = do x <- lift $ readline "Idris> "
23+ = do x <- lift $ readline (prompt ++ "> ")
23 case x of
24 case x of
24− Nothing -> repl
25+ Nothing -> repl prompt
25 Just input -> do lift $ addHistory input
26 Just input -> do lift $ addHistory input
26 continue <- processInput input
27 continue <- processInput input
27− when continue repl
28+ when continue (repl prompt)
28
29
29processInput :: String -> Idris Bool
30processInput :: String -> Idris Bool
30processInput cmd
31processInput cmd
src/Main.hs+19−3
@@ -6,6 +6,7 @@ import System.Environment
6import System.Exit
6import System.Exit
7
7
8import Data.Maybe
8import Data.Maybe
9+import Data.Version
9import Control.Monad.State
10import Control.Monad.State
10
11
11import Core.CoreParser
12import Core.CoreParser
@@ -21,6 +22,7 @@ import Idris.REPL
21import Idris.ElabDecls
22import Idris.ElabDecls
22import Idris.Primitives
23import Idris.Primitives
23import Idris.Imports
24import Idris.Imports
25+import Paths_miniidris
24
26
25-- Main program reads command line options, parses the main program, and gets
27-- Main program reads command line options, parses the main program, and gets
26-- on with the REPL.
28-- on with the REPL.
@@ -41,13 +43,19 @@ runIdris opts =
41 do let inputs = opt getFile opts
43 do let inputs = opt getFile opts
42 mapM_ makeOption opts
44 mapM_ makeOption opts
43 elabPrims
45 elabPrims
44− when (not (NoPrelude `elem` opts)) $ loadModule "prelude"
46+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
47+ return ()
45− mapM_ loadModule inputs
48+ mods <- mapM loadModule inputs
46− when (not (NoREPL `elem` opts)) $ repl
49+ when (not (NoREPL `elem` opts)) $ do iputStrLn banner
50+ repl (mkPrompt mods)
47 where
51 where
48 makeOption (OLogging i) = setLogLevel i
52 makeOption (OLogging i) = setLogLevel i
49 makeOption _ = return ()
53 makeOption _ = return ()
50
54
55+mkPrompt [] = "Idris"
56+mkPrompt [x] = "*" ++ x
57+mkPrompt (x:xs) = "*" ++ x ++ " " ++ mkPrompt xs
58+
51getFile :: Opt -> Maybe String
59getFile :: Opt -> Maybe String
52getFile (Filename str) = Just str
60getFile (Filename str) = Just str
53getFile _ = Nothing
61getFile _ = Nothing
@@ -79,3 +87,11 @@ main'
79 err -> print err
87 err -> print err
80 -}
88 -}
81
89
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+