@@ -127,9 +127,13 @@ prove mode opt ctxt lit n ty
127 _ -> return ()
127 _ -> return ()
129elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
129elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
130−elabStep st e = case runStateT eCheck st of
131+ case runStateT eCheck st of
131− OK (a, st') -> return (a, st')
132+ OK ((a, ctxt'), ES (ps, est@EState{new_tyDecls = declTodo}) x old) ->
134+ processTacticDecls toplevel declTodo
135+ return (a, ES (ps, est {new_tyDecls = []}) x old)
132− Error a -> ierror a
136+ Error a -> ierror a
133 where eCheck = do res <- e
137 where eCheck = do res <- e
134 matchProblems True
138 matchProblems True
135 unifyProblems
139 unifyProblems
@@ -138,7 +142,7 @@ elabStep st e = case runStateT eCheck st of
138 [] -> do tm <- get_term
142 [] -> do tm <- get_term
139 ctxt <- get_context
143 ctxt <- get_context
140 lift $ check ctxt [] (forget tm)
144 lift $ check ctxt [] (forget tm)
141− return res
145+ return (res, ctxt)
142 ((_,_,_,_,e,_,_):_) -> lift $ Error e
146 ((_,_,_,_,e,_,_):_) -> lift $ Error e
144dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
148dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
@@ -265,6 +269,7 @@ undoElab prf env st [] = ifail "Nothing to undo"
265undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
269undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
266 return (prf', env', st', hs)
270 return (prf', env', st', hs)
268elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
273elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
269elabloop fn d prompt prf e prev h env
274elabloop fn d prompt prf e prev h env
270 = do ist <- getIState
275 = do ist <- getIState