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