@@ -461,12 +461,15 @@ process h fn (Eval t)
461461process h fn (ExecVal t)
462462 = do ctxt <- getContext
463463 ist <- getIState
464+ let imp = opt_showimp (idris_options ist)
464465 (tm, ty) <- elabVal toplevel False t
465466-- let tm' = normaliseAll ctxt [] tm
466467 let ty' = normaliseAll ctxt [] ty
467468 res <- execute tm
468− ihPrintResult h (showTm ist (delab ist res) ++ " : " ++
469− showTm ist (delab ist ty'))
469+ let (resOut, tyOut) = (prettyImp imp (delab ist res),
470+ prettyImp imp (delab ist ty'))
471+ ihPrintTermWithType h resOut tyOut
472+
470473process h fn (Check (PRef _ n))
471474 = do ctxt <- getContext
472475 ist <- getIState