@@ -397,17 +397,41 @@ ihPrintResult h s = do i <- getIState
397397 let good = SexpList [SymbolAtom "ok", toSExp s] in
398398 runIO $ hPutStrLn h $ convSExp "return" good n
399399
400+-- | Write a pretty-printed term to the console with semantic coloring
401+consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
402+consoleDisplayAnnotated h output = do ist <- getIState
403+ runIO . hPutStrLn h .
404+ displayDecorated (consoleDecorate ist) .
405+ renderCompact $ output
406+
407+-- | Write pretty-printed output to IDESlave with semantic annotations
408+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
409+ideSlaveReturnAnnotated n h out = do ist <- getIState
410+ let (str, spans) = displaySpans .
411+ renderCompact .
412+ fmap (fancifyAnnots ist) $
413+ out
414+ good = [SymbolAtom "ok", toSExp str, toSExp spans]
415+ runIO . hPutStrLn h $ convSExp "return" good n
416+
400417ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
401418ihPrintTermWithType h tm ty = do ist <- getIState
402419 let output = tm <+> colon <+> ty
403420 case idris_outputmode ist of
404− RawOutput -> runIO .
405− hPutStrLn h .
406− displayDecorated (consoleDecorate ist) .
407− renderCompact $ output
408− IdeSlave n -> let (str, spans) = displaySpans (fmap (fancifyAnnots ist) (renderCompact output))
409− good = [SymbolAtom "ok", toSExp str, toSExp spans]
410− in runIO . hPutStrLn h $ convSExp "return" good n
421+ RawOutput -> consoleDisplayAnnotated h output
422+ IdeSlave n -> ideSlaveReturnAnnotated n h output
423+
424+-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
425+ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()
426+ihPrintFunTypes h n [] = ihPrintError h $ "No such variable " ++ show n
427+ihPrintFunTypes h n overloads = do imp <- impShow
428+ ist <- getIState
429+ let output = vsep (map (uncurry (ppOverload imp)) overloads)
430+ case idris_outputmode ist of
431+ RawOutput -> consoleDisplayAnnotated h output
432+ IdeSlave n -> ideSlaveReturnAnnotated n h output
433+ where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
434+ ppOverload imp n tm = fullName n <+> colon <+> prettyImp imp tm
411435
412436fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
413437fancifyAnnots ist annot@(AnnName n _ _) =