git.iko.soy/Idris-dev
on master help sign in
Use pretty-printer to display :t for metavars
106061dDavid Raymond Christiansen
src/Idris/AbsSyntax.hs+9−3
compare with master
unifiedsplit
@@ -417,9 +417,9 @@ setWidth w = do ist <- getIState
417iRender :: Doc a -> Idris (SimpleDoc a)
417iRender :: Doc a -> Idris (SimpleDoc a)
418iRender d = do w <- getWidth
418iRender d = do w <- getWidth
419 return $ case w of
419 return $ case w of
420− InfinitelyWide -> renderCompact d
420+ InfinitelyWide -> renderPretty 1.0 1000000000 d
421 ColsWide n -> if n < 1
421 ColsWide n -> if n < 1
422− then renderCompact d
422+ then renderPretty 1.0 1000000000 d
423 else renderPretty 0.5 n d
423 else renderPretty 0.5 n d
424
424
425ihPrintResult :: Handle -> String -> Idris ()
425ihPrintResult :: Handle -> String -> Idris ()
@@ -445,7 +445,7 @@ consoleDisplayAnnotated h output = do ist <- getIState
445ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
445ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
446ideSlaveReturnAnnotated n h out = do ist <- getIState
446ideSlaveReturnAnnotated n h out = do ist <- getIState
447 let (str, spans) = displaySpans .
447 let (str, spans) = displaySpans .
448− renderCompact .
448+ renderPretty 0.8 80 .
449 fmap (fancifyAnnots ist) $
449 fmap (fancifyAnnots ist) $
450 out
450 out
451 good = [SymbolAtom "ok", toSExp str, toSExp spans]
451 good = [SymbolAtom "ok", toSExp str, toSExp spans]
@@ -470,6 +470,12 @@ ihPrintFunTypes h n overloads = do imp <- impShow
470 where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
470 where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
471 ppOverload imp n tm = fullName n <+> colon <+> align (prettyImp imp tm)
471 ppOverload imp n tm = fullName n <+> colon <+> align (prettyImp imp tm)
472
472
473+ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
474+ihRenderResult h d = do ist <- getIState
475+ case idris_outputmode ist of
476+ RawOutput -> consoleDisplayAnnotated h d
477+ IdeSlave n -> ideSlaveReturnAnnotated n h d
478+
473fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
479fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
474fancifyAnnots ist annot@(AnnName n _ _) =
480fancifyAnnots ist annot@(AnnName n _ _) =
475 do let ctxt = tt_ctxt ist
481 do let ctxt = tt_ctxt ist
src/Idris/REPL.hs+22−18
@@ -14,7 +14,7 @@ import Idris.Parser
14import Idris.Primitives
14import Idris.Primitives
15import Idris.Coverage
15import Idris.Coverage
16import Idris.UnusedArgs
16import Idris.UnusedArgs
17−import Idris.Docs
17+import Idris.Docs hiding (Doc)
18import Idris.Help
18import Idris.Help
19import Idris.Completion
19import Idris.Completion
20import qualified Idris.IdeSlave as IdeSlave
20import qualified Idris.IdeSlave as IdeSlave
@@ -30,6 +30,7 @@ import Version_idris (gitHash)
30import Util.System
30import Util.System
31import Util.DynamicLinker
31import Util.DynamicLinker
32import Util.Net (listenOnLocalhost)
32import Util.Net (listenOnLocalhost)
33+import Util.Pretty hiding ((</>))
33
34
34import Idris.Core.Evaluate
35import Idris.Core.Evaluate
35import Idris.Core.Execute (execute)
36import Idris.Core.Execute (execute)
@@ -470,32 +471,35 @@ process h fn (Check (PRef _ n))
470 = do ctxt <- getContext
471 = do ctxt <- getContext
471 ist <- getIState
472 ist <- getIState
472 imp <- impShow
473 imp <- impShow
473− c <- colourise
474 case lookupNames n ctxt of
474 case lookupNames n ctxt of
475 ts@(t:_) ->
475 ts@(t:_) ->
476 case lookup t (idris_metavars ist) of
476 case lookup t (idris_metavars ist) of
477+ Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
477− Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
478+ showMetavarInfo imp ist n i
478 Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)
479 Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)
479 [] -> ihPrintError h $ "No such variable " ++ show n
480 [] -> ihPrintError h $ "No such variable " ++ show n
480 where
481 where
481− showMetavarInfo c imp ist n i
482+ showMetavarInfo imp ist n i
482 = case lookupTy n (tt_ctxt ist) of
483 = case lookupTy n (tt_ctxt ist) of
483− (ty:_) -> putTy c imp ist i (delab ist ty)
484+ (ty:_) -> putTy imp ist i [] (delab ist ty)
485+ putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
484− putTy c imp ist 0 sc = putGoal c imp ist sc
486+ putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
485− putTy c imp ist i (PPi _ n t sc)
487+ putTy imp ist i bnd (PPi _ n t sc)
486− = let current = " " ++
488+ = let current = text " " <>
487 (case n of
489 (case n of
488− MN _ _ -> "_"
490+ MN _ _ -> text "_"
489− UN nm | ('_':'_':_) <- str nm -> "_"
491+ UN nm | ('_':'_':_) <- str nm -> text "_"
490− _ -> showName (Just ist) [] False c n) ++
492+ _ -> bindingOf n False) <+>
491− " : " ++ showTm ist t ++ "\n"
493+ colon <+> align (tPretty bnd ist t) <> line
492 in
494 in
493− current ++ putTy c imp ist (i-1) sc
495+ current <> putTy imp ist (i-1) ((n,False):bnd) sc
494− putTy c imp ist _ sc = putGoal c imp ist sc
496+ putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc
495− putGoal c imp ist g
497+ putGoal imp ist bnd g
496− = "--------------------------------------\n" ++
498+ = text "--------------------------------------" <$>
497− showName (Just ist) [] False c n ++ " : " ++
499+ annotate (AnnName n Nothing Nothing) (text $ show n) <+> colon <+>
498− showTm ist g
500+ align (tPretty bnd ist g)
501+
502+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd t
499
503
500
504
501process h fn (Check t)
505process h fn (Check t)