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