@@ -56,16 +56,17 @@ processInput cmd orig inputs
57 mods <- mapM loadModule inputs
57 mods <- mapM loadModule inputs
58 return (Just inputs)
58 return (Just inputs)
59+ Right Edit -> do edit fn orig
59 Right Quit -> do iputStrLn "Bye bye"
61 Right Quit -> do iputStrLn "Bye bye"
60 return Nothing
62 return Nothing
61− Right cmd -> do idrisCatch (process fn cmd)
63+ Right cmd -> do idrisCatch (process cmd)
62 (\e -> iputStrLn (report e))
64 (\e -> iputStrLn (report e))
63 return (Just inputs)
65 return (Just inputs)
65−process :: FilePath -> Command -> Idris ()
67+edit :: FilePath -> IState -> Idris ()
66−process _ Help = iputStrLn displayHelp
67−process "" Edit = iputStrLn "Nothing to edit"
68+edit "" orig = iputStrLn "Nothing to edit"
68−process f Edit
69+edit f orig
69 = do i <- get
70 = do i <- get
70 env <- lift $ getEnvironment
71 env <- lift $ getEnvironment
71 let editor = getEditor env
72 let editor = getEditor env
@@ -74,54 +75,60 @@ process f Edit
74 Nothing -> " "
75 Nothing -> " "
75 let cmd = editor ++ line ++ f
76 let cmd = editor ++ line ++ f
76 lift $ system cmd
77 lift $ system cmd
79+ put (orig { idris_options = idris_options i })
78 where getEditor env | Just ed <- lookup "EDITOR" env = ed
82 where getEditor env | Just ed <- lookup "EDITOR" env = ed
79 | Just ed <- lookup "VISUAL" env = ed
83 | Just ed <- lookup "VISUAL" env = ed
80 | otherwise = "vi"
84 | otherwise = "vi"
86+process :: Command -> Idris ()
87+process Help = iputStrLn displayHelp
81−process _ (Eval t) = do (tm, ty) <- elabVal toplevel False t
88+process (Eval t) = do (tm, ty) <- elabVal toplevel False t
82− ctxt <- getContext
89+ ctxt <- getContext
83− ist <- get
90+ ist <- get
84− let tm' = normaliseC ctxt [] tm
91+ let tm' = normaliseC ctxt [] tm
85− let ty' = normaliseC ctxt [] ty
92+ let ty' = normaliseC ctxt [] ty
86− logLvl 3 $ "Raw: " ++ show (tm', ty')
93+ logLvl 3 $ "Raw: " ++ show (tm', ty')
87− iputStrLn (show (delab ist tm') ++ " : " ++
94+ iputStrLn (show (delab ist tm') ++ " : " ++
88− show (delab ist ty'))
95+ show (delab ist ty'))
89−process x (Check (PRef _ n))
96+process (Check (PRef _ n))
90− = process x (Check (PQuote (Var n)))
97+ = process (Check (PQuote (Var n)))
91−process _ (Check t) = do (tm, ty) <- elabVal toplevel False t
98+process (Check t) = do (tm, ty) <- elabVal toplevel False t
92− ctxt <- getContext
99+ ctxt <- getContext
93− ist <- get
100+ ist <- get
94− let ty' = normaliseC ctxt [] ty
101+ let ty' = normaliseC ctxt [] ty
95− iputStrLn (show (delab ist tm) ++ " : " ++
102+ iputStrLn (show (delab ist tm) ++ " : " ++
96− show (delab ist ty'))
103+ show (delab ist ty'))
97−process _ (Defn n) = do ctxt <- getContext
104+process (Defn n) = do ctxt <- getContext
98− lift $ print (lookupDef n ctxt)
105+ lift $ print (lookupDef n ctxt)
99−process _ (Spec t) = do (tm, ty) <- elabVal toplevel False t
106+process (Spec t) = do (tm, ty) <- elabVal toplevel False t
100− ctxt <- getContext
107+ ctxt <- getContext
101− ist <- get
108+ ist <- get
102− let tm' = specialise ctxt (idris_statics ist) tm
109+ let tm' = specialise ctxt (idris_statics ist) tm
103− iputStrLn (show (delab ist tm'))
110+ iputStrLn (show (delab ist tm'))
104−process _ (Prove n) = prover n
111+process (Prove n) = prover n
105−process _ (HNF t) = do (tm, ty) <- elabVal toplevel False t
112+process (HNF t) = do (tm, ty) <- elabVal toplevel False t
106− ctxt <- getContext
113+ ctxt <- getContext
107− ist <- get
114+ ist <- get
108− let tm' = simplify ctxt [] tm
115+ let tm' = simplify ctxt [] tm
109− iputStrLn (show (delab ist tm'))
116+ iputStrLn (show (delab ist tm'))
110−process _ TTShell = do ist <- get
117+process TTShell = do ist <- get
111− let shst = initState (tt_ctxt ist)
118+ let shst = initState (tt_ctxt ist)
112− shst' <- lift $ runShell shst
119+ shst' <- lift $ runShell shst
113− return ()
120+ return ()
114−process _ (Execute f) = do compile f
121+process (Execute f) = do compile f
115− lift $ system ("./" ++ f)
122+ lift $ system ("./" ++ f)
116− return ()
123+ return ()
117−process _ (Compile f) = do compile f
124+process (Compile f) = do compile f
118−process _ (LogLvl i) = setLogLevel i
125+process (LogLvl i) = setLogLevel i
119−process _ Metavars = do ist <- get
126+process Metavars = do ist <- get
120− let mvs = idris_metavars ist \\ primDefs
127+ let mvs = idris_metavars ist \\ primDefs
121− case mvs of
128+ case mvs of
122− [] -> iputStrLn "No global metavariables to solve"
129+ [] -> iputStrLn "No global metavariables to solve"
123− _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
130+ _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
124−process _ NOP = return ()
131+process NOP = return ()
126displayHelp = let vstr = showVersion version in
133displayHelp = let vstr = showVersion version in
127 "\nIdris version " ++ vstr ++ "\n" ++
134 "\nIdris version " ++ vstr ++ "\n" ++