@@ -204,34 +204,35 @@ ploop fn d prompt prf e h
204 case cmd of
204 case cmd of
205 Success Abandon -> do iPrintError ""; ifail "Abandoned"
205 Success Abandon -> do iPrintError ""; ifail "Abandoned"
206 _ -> return ()
206 _ -> return ()
207− (d, st, done, prf') <- idrisCatch
207+ (d, st, done, prf', res) <- idrisCatch
208 (case cmd of
208 (case cmd of
209− Failure err -> do iPrintError (show err)
210− return (False, e, False, prf)
209+ Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
211 Success Undo -> do (_, st) <- elabStep e loadState
210 Success Undo -> do (_, st) <- elabStep e loadState
212− return (True, st, False, init prf)
211+ return (True, st, False, init prf, Right "")
213− Success ProofState -> return (True, e, False, prf)
212+ Success ProofState -> return (True, e, False, prf, Right "")
214 Success ProofTerm -> do tm <- lifte e get_term
213 Success ProofTerm -> do tm <- lifte e get_term
215 iputStrLn $ "TT: " ++ show tm ++ "\n"
214 iputStrLn $ "TT: " ++ show tm ++ "\n"
216− return (False, e, False, prf)
215+ return (False, e, False, prf, Right "")
217 Success Qed -> do hs <- lifte e get_holes
216 Success Qed -> do hs <- lifte e get_holes
218 when (not (null hs)) $ ifail "Incomplete proof"
217 when (not (null hs)) $ ifail "Incomplete proof"
219 iputStrLn "Proof completed!"
218 iputStrLn "Proof completed!"
220− return (False, e, True, prf)
219+ return (False, e, True, prf, Right "")
221 Success (TCheck (PRef _ n)) -> checkNameType n
220 Success (TCheck (PRef _ n)) -> checkNameType n
222 Success (TCheck t) -> checkType t
221 Success (TCheck t) -> checkType t
223 Success (TEval t) -> evalTerm t e
222 Success (TEval t) -> evalTerm t e
224 Success tac -> do (_, e) <- elabStep e saveState
223 Success tac -> do (_, e) <- elabStep e saveState
225 (_, st) <- elabStep e (runTac autoSolve i fn tac)
224 (_, st) <- elabStep e (runTac autoSolve i fn tac)
226−-- trace (show (problems (proof st))) $
227− return (True, st, False, prf ++ [step]))
225+ return (True, st, False, prf ++ [step], Right ""))
228− (\err -> do iPrintError (pshow i err)
229− return (False, e, False, prf))
226+ (\err -> return (False, e, False, prf, Left err))
230 ideslavePutSExp "write-proof-state" (prf', length prf')
227 ideslavePutSExp "write-proof-state" (prf', length prf')
229+ Left err -> do iPrintError (pshow i err)
230+ ploop fn d prompt prf' st h'
231− if done then do (tm, _) <- elabStep st get_term
232+ if done then do (tm, _) <- elabStep st get_term
232− return (tm, prf')
233+ return (tm, prf')
233− else do iPrintResult ""
234+ else do iPrintResult ok
234− ploop fn d prompt prf' st h'
235+ ploop fn d prompt prf' st h'
235 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
236 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
236 checkNameType n = do
237 checkNameType n = do
237 ctxt <- getContext
238 ctxt <- getContext
@@ -250,7 +251,7 @@ ploop fn d prompt prf e h
250 [] -> ihPrintError h $ "No such variable " ++ show n
251 [] -> ihPrintError h $ "No such variable " ++ show n
251 ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
252 ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
252 putIState ist
253 putIState ist
253− return (False, e, False, prf))
254+ return (False, e, False, prf, Right ""))
254 (\err -> do putIState ist ; ierror err)
255 (\err -> do putIState ist ; ierror err)
256 checkType t = do
257 checkType t = do
@@ -272,7 +273,7 @@ ploop fn d prompt prf e h
272 ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
273 ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
273 (pprintPTerm ppo bnd [] infixes (delab ist ty))
274 (pprintPTerm ppo bnd [] infixes (delab ist ty))
274 putIState ist
275 putIState ist
275− return (False, e, False, prf))
276+ return (False, e, False, prf, Right ""))
276 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
277 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
278 evalTerm t e = withErrorReflection $
279 evalTerm t e = withErrorReflection $
@@ -293,5 +294,5 @@ ploop fn d prompt prf e h
293 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
294 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
294 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
295 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
295 putIState ist
296 putIState ist
296− return (False, e, False, prf))
297+ return (False, e, False, prf, Right ""))
297 (\err -> do putIState ist ; ierror err)
298 (\err -> do putIState ist ; ierror err)