@@ -9,69 +9,102 @@ import Idris.Error
99import Idris.Delaborate
1010import Idris.Compiler
1111import Idris.Prover
12+import Idris.Parser
1213
1314import Core.Evaluate
1415import Core.ProofShell
1516import Core.TT
1617
1718import System.Console.Readline
19+import System.FilePath
20+import System.Environment
21+import System.Process
1822import Control.Monad
1923import Control.Monad.State
2024import Data.List
25+import Data.Char
2126
22−repl :: String -> Idris ()
23−repl prompt
24− = do x <- lift $ readline (prompt ++ "> ")
27+repl :: IState -> [FilePath] -> Idris ()
28+repl orig mods
29+ = do let prompt = mkPrompt mods
30+ x <- lift $ readline (prompt ++ "> ")
2531 case x of
26− Nothing -> repl prompt
32+ Nothing -> repl orig mods
2733 Just input -> do lift $ addHistory input
28− continue <- processInput input
29− when continue (repl prompt)
34+ ms <- processInput input orig mods
35+ case ms of
36+ Just mods -> repl orig mods
37+ Nothing -> return ()
3038
31−processInput :: String -> Idris Bool
32−processInput cmd
39+mkPrompt [] = "Idris"
40+mkPrompt [x] = "*" ++ dropExtension x
41+mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
42+
43+processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])
44+processInput cmd orig inputs
3345 = do i <- get
46+ let fn = case inputs of
47+ (f:_) -> f
48+ _ -> ""
3449 case parseCmd i cmd of
3550 Left err -> do lift $ print err
36− return True
51+ return (Just inputs)
52+ Right Reload -> do put orig
53+ clearErr
54+ mods <- mapM loadModule inputs
55+ return (Just inputs)
3756 Right Quit -> do iputStrLn "Bye bye"
38− return False
39− Right cmd -> do idrisCatch (process cmd)
57+ return Nothing
58+ Right cmd -> do idrisCatch (process fn cmd)
4059 (\e -> iputStrLn (report e))
41− return True
42−
43−process :: Command -> Idris ()
44−process Help
60+ return (Just inputs)
61+
62+process :: FilePath -> Command -> Idris ()
63+process _ Help
4564 = iputStrLn "At some point I'll write some help text. Thanks for asking though."
46−process (Eval t) = do (tm, ty) <- elabVal toplevel t
47− ctxt <- getContext
48− ist <- get
49− let tm' = normaliseC ctxt [] tm
50− let ty' = normaliseC ctxt [] ty
51− logLvl 3 $ "Raw: " ++ show (tm', ty')
52− iputStrLn (show (delab ist tm') ++ " : " ++
53− show (delab ist ty'))
54−process (Spec t) = do (tm, ty) <- elabVal toplevel t
55− ctxt <- getContext
56− ist <- get
57− let tm' = specialise ctxt (idris_statics ist) tm
58− iputStrLn (show (delab ist tm'))
59−process (Prove n) = prover n
60−process (HNF t) = do (tm, ty) <- elabVal toplevel t
61− ctxt <- getContext
62− ist <- get
63− let tm' = hnf ctxt [] tm
64− iputStrLn (show (delab ist tm'))
65−process TTShell = do ist <- get
66− let shst = initState (tt_ctxt ist)
67− shst' <- lift $ runShell shst
68− return ()
69−process (Compile f) = do compile f
70−process (LogLvl i) = setLogLevel i
71−process Metavars = do ist <- get
72− let mvs = idris_metavars ist \\ primDefs
73− case mvs of
74− [] -> iputStrLn "No global metavariables to solve"
75− _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
76−process NOP = return ()
65+process "" Edit = iputStrLn "Nothing to edit"
66+process f Edit
67+ = do i <- get
68+ env <- lift $ getEnvironment
69+ let editor = getEditor env
70+ let line = case errLine i of
71+ Just l -> " +" ++ show l ++ " "
72+ Nothing -> " "
73+ let cmd = editor ++ line ++ f
74+ lift $ system cmd
75+ return ()
76+ where getEditor env | Just ed <- lookup "EDITOR" env = ed
77+ | Just ed <- lookup "VISUAL" env = ed
78+ | otherwise = "vi"
79+process _ (Eval t) = do (tm, ty) <- elabVal toplevel t
80+ ctxt <- getContext
81+ ist <- get
82+ let tm' = normaliseC ctxt [] tm
83+ let ty' = normaliseC ctxt [] ty
84+ logLvl 3 $ "Raw: " ++ show (tm', ty')
85+ iputStrLn (show (delab ist tm') ++ " : " ++
86+ show (delab ist ty'))
87+process _ (Spec t) = do (tm, ty) <- elabVal toplevel t
88+ ctxt <- getContext
89+ ist <- get
90+ let tm' = specialise ctxt (idris_statics ist) tm
91+ iputStrLn (show (delab ist tm'))
92+process _ (Prove n) = prover n
93+process _ (HNF t) = do (tm, ty) <- elabVal toplevel t
94+ ctxt <- getContext
95+ ist <- get
96+ let tm' = hnf ctxt [] tm
97+ iputStrLn (show (delab ist tm'))
98+process _ TTShell = do ist <- get
99+ let shst = initState (tt_ctxt ist)
100+ shst' <- lift $ runShell shst
101+ return ()
102+process _ (Compile f) = do compile f
103+process _ (LogLvl i) = setLogLevel i
104+process _ Metavars = do ist <- get
105+ let mvs = idris_metavars ist \\ primDefs
106+ case mvs of
107+ [] -> iputStrLn "No global metavariables to solve"
108+ _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
109+process _ NOP = return ()
77110