@@ -204,34 +204,35 @@ ploop fn d prompt prf e h
204204 case cmd of
205205 Success Abandon -> do iPrintError ""; ifail "Abandoned"
206206 _ -> return ()
207− (d, st, done, prf') <- idrisCatch
207+ (d, st, done, prf', res) <- idrisCatch
208208 (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)
211210 Success Undo -> do (_, st) <- elabStep e loadState
212− return (True, st, False, init prf)
213− Success ProofState -> return (True, e, False, prf)
211+ return (True, st, False, init prf, Right "")
212+ Success ProofState -> return (True, e, False, prf, Right "")
214213 Success ProofTerm -> do tm <- lifte e get_term
215214 iputStrLn $ "TT: " ++ show tm ++ "\n"
216− return (False, e, False, prf)
215+ return (False, e, False, prf, Right "")
217216 Success Qed -> do hs <- lifte e get_holes
218217 when (not (null hs)) $ ifail "Incomplete proof"
219218 iputStrLn "Proof completed!"
220− return (False, e, True, prf)
219+ return (False, e, True, prf, Right "")
221220 Success (TCheck (PRef _ n)) -> checkNameType n
222221 Success (TCheck t) -> checkType t
223222 Success (TEval t) -> evalTerm t e
224223 Success tac -> do (_, e) <- elabStep e saveState
225224 (_, st) <- elabStep e (runTac autoSolve i fn tac)
226−-- trace (show (problems (proof st))) $
227− return (True, st, False, prf ++ [step]))
228− (\err -> do iPrintError (pshow i err)
229− return (False, e, False, prf))
225+ return (True, st, False, prf ++ [step], Right ""))
226+ (\err -> return (False, e, False, prf, Left err))
230227 ideslavePutSExp "write-proof-state" (prf', length prf')
231− if done then do (tm, _) <- elabStep st get_term
232− return (tm, prf')
233− else do iPrintResult ""
234− ploop fn d prompt prf' st h'
228+ case res of
229+ Left err -> do iPrintError (pshow i err)
230+ ploop fn d prompt prf' st h'
231+ Right ok ->
232+ if done then do (tm, _) <- elabStep st get_term
233+ return (tm, prf')
234+ else do iPrintResult ok
235+ ploop fn d prompt prf' st h'
235236 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
236237 checkNameType n = do
237238 ctxt <- getContext
@@ -250,7 +251,7 @@ ploop fn d prompt prf e h
250251 [] -> ihPrintError h $ "No such variable " ++ show n
251252 ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
252253 putIState ist
253− return (False, e, False, prf))
254+ return (False, e, False, prf, Right ""))
254255 (\err -> do putIState ist ; ierror err)
255256
256257 checkType t = do
@@ -272,7 +273,7 @@ ploop fn d prompt prf e h
272273 ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
273274 (pprintPTerm ppo bnd [] infixes (delab ist ty))
274275 putIState ist
275− return (False, e, False, prf))
276+ return (False, e, False, prf, Right ""))
276277 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
277278
278279 evalTerm t e = withErrorReflection $
@@ -293,5 +294,5 @@ ploop fn d prompt prf e h
293294 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
294295 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
295296 putIState ist
296− return (False, e, False, prf))
297+ return (False, e, False, prf, Right ""))
297298 (\err -> do putIState ist ; ierror err)