@@ -461,12 +461,15 @@ process h fn (Eval t)
461process h fn (ExecVal t)
461process h fn (ExecVal t)
462 = do ctxt <- getContext
462 = do ctxt <- getContext
463 ist <- getIState
463 ist <- getIState
464+ let imp = opt_showimp (idris_options ist)
464 (tm, ty) <- elabVal toplevel False t
465 (tm, ty) <- elabVal toplevel False t
465-- let tm' = normaliseAll ctxt [] tm
466-- let tm' = normaliseAll ctxt [] tm
466 let ty' = normaliseAll ctxt [] ty
467 let ty' = normaliseAll ctxt [] ty
467 res <- execute tm
468 res <- execute tm
468− ihPrintResult h (showTm ist (delab ist res) ++ " : " ++
469+ let (resOut, tyOut) = (prettyImp imp (delab ist res),
469− showTm ist (delab ist ty'))
470+ prettyImp imp (delab ist ty'))
471+ ihPrintTermWithType h resOut tyOut
470process h fn (Check (PRef _ n))
473process h fn (Check (PRef _ n))
471 = do ctxt <- getContext
474 = do ctxt <- getContext
472 ist <- getIState
475 ist <- getIState