@@ -127,9 +127,13 @@ prove mode opt ctxt lit n ty
127127 _ -> return ()
128128
129129elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
130−elabStep st e = case runStateT eCheck st of
131− OK (a, st') -> return (a, st')
132− Error a -> ierror a
130+elabStep st e =
131+ case runStateT eCheck st of
132+ OK ((a, ctxt'), ES (ps, est@EState{new_tyDecls = declTodo}) x old) ->
133+ do setContext ctxt'
134+ processTacticDecls toplevel declTodo
135+ return (a, ES (ps, est {new_tyDecls = []}) x old)
136+ Error a -> ierror a
133137 where eCheck = do res <- e
134138 matchProblems True
135139 unifyProblems
@@ -138,7 +142,7 @@ elabStep st e = case runStateT eCheck st of
138142 [] -> do tm <- get_term
139143 ctxt <- get_context
140144 lift $ check ctxt [] (forget tm)
141− return res
145+ return (res, ctxt)
142146 ((_,_,_,_,e,_,_):_) -> lift $ Error e
143147
144148dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
@@ -265,6 +269,7 @@ undoElab prf env st [] = ifail "Nothing to undo"
265269undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
266270 return (prf', env', st', hs)
267271
272+
268273elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
269274elabloop fn d prompt prf e prev h env
270275 = do ist <- getIState