@@ -251,7 +251,8 @@ ploop fn d prompt prf e h
251 (\err -> return (False, e, False, prf, Left err))
251 (\err -> return (False, e, False, prf, Left err))
252 ideslavePutSExp "write-proof-state" (prf', length prf')
252 ideslavePutSExp "write-proof-state" (prf', length prf')
253 case res of
253 case res of
254− Left err -> do iPrintError (pshow i err)
254+ Left err -> do ist <- getIState
255+ iRenderError $ pprintErr ist err
255 ploop fn d prompt prf' st h'
256 ploop fn d prompt prf' st h'
256 Right ok ->
257 Right ok ->
257 if done then do (tm, _) <- elabStep st get_term
258 if done then do (tm, _) <- elabStep st get_term