git.iko.soy/Idris-dev
on master help sign in
More IDESlave semantic highlighting
de72eb9David Raymond Christiansen
src/Idris/AbsSyntax.hs+31−7
compare with master
unifiedsplit
@@ -397,17 +397,41 @@ ihPrintResult h s = do i <- getIState
397 let good = SexpList [SymbolAtom "ok", toSExp s] in
397 let good = SexpList [SymbolAtom "ok", toSExp s] in
398 runIO $ hPutStrLn h $ convSExp "return" good n
398 runIO $ hPutStrLn h $ convSExp "return" good n
399
399
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+
400ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
417ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
401ihPrintTermWithType h tm ty = do ist <- getIState
418ihPrintTermWithType h tm ty = do ist <- getIState
402 let output = tm <+> colon <+> ty
419 let output = tm <+> colon <+> ty
403 case idris_outputmode ist of
420 case idris_outputmode ist of
404− RawOutput -> runIO .
421+ RawOutput -> consoleDisplayAnnotated h output
405− hPutStrLn h .
422+ IdeSlave n -> ideSlaveReturnAnnotated n h output
406− displayDecorated (consoleDecorate ist) .
423+
407− renderCompact $ output
424+-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
408− IdeSlave n -> let (str, spans) = displaySpans (fmap (fancifyAnnots ist) (renderCompact output))
425+ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()
409− good = [SymbolAtom "ok", toSExp str, toSExp spans]
426+ihPrintFunTypes h n [] = ihPrintError h $ "No such variable " ++ show n
410− in runIO . hPutStrLn h $ convSExp "return" good 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
411
435
412fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
436fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
413fancifyAnnots ist annot@(AnnName n _ _) =
437fancifyAnnots ist annot@(AnnName n _ _) =
src/Idris/REPL.hs+1−3
@@ -471,9 +471,7 @@ process h fn (Check (PRef _ n))
471 ts@(t:_) ->
471 ts@(t:_) ->
472 case lookup t (idris_metavars ist) of
472 case lookup t (idris_metavars ist) of
473 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
473 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
474− Nothing -> ihPrintResult h $
475− concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++
476− showTm ist (delabTy ist n)) $ ts
474+ Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)
477 [] -> ihPrintError h $ "No such variable " ++ show n
475 [] -> ihPrintError h $ "No such variable " ++ show n
478 where
476 where
479 showMetavarInfo c imp ist n i
477 showMetavarInfo c imp ist n i