git.iko.soy/Idris-dev
on master help sign in
Use pretty-printer for :i command
f927e7fDavid Raymond Christiansen
src/Idris/REPL.hs+19−23
compare with master
unifiedsplit
@@ -617,7 +617,8 @@ process h fn (DebugInfo n)
617process h fn (Info n)
617process h fn (Info n)
618 = do i <- getIState
618 = do i <- getIState
619 case lookupCtxt n (idris_classes i) of
619 case lookupCtxt n (idris_classes i) of
620− [c] -> classInfo c
620+ [c] -> do info <- classInfo c
621+ ihRenderResult h info
621 _ -> iPrintError "Not a class"
622 _ -> iPrintError "Not a class"
622process h fn (Search t) = iPrintError "Not implemented"
623process h fn (Search t) = iPrintError "Not implemented"
623-- FIXME: There is far too much repetition in the cases below!
624-- FIXME: There is far too much repetition in the cases below!
@@ -993,28 +994,23 @@ process h fn (Apropos a) =
993 isUN (NS n _) = isUN n
994 isUN (NS n _) = isUN n
994 isUN _ = False
995 isUN _ = False
995
996
996−classInfo :: ClassInfo -> Idris ()
997+classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)
997−classInfo ci = do iputStrLn "Methods:\n"
998+classInfo ci = do ist <- getIState
999+ ctxt <- getContext
1000+ return $
1001+ text "Methods:" <> line <>
998− mapM_ dumpMethod (class_methods ci)
1002+ vsep (map (dumpMethod ist) (class_methods ci)) <> line <> line <>
999− iputStrLn ""
1000− iputStrLn "Default superclass instances:\n"
1003+ text "Default superclass instances:" <> line <>
1001− mapM_ dumpDefaultInstance (class_default_superclasses ci)
1004+ vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci)) <> line <>
1002− iputStrLn ""
1003− iputStrLn "Instances:\n"
1005+ text "Instances:" <> line <>
1004− mapM_ dumpInstance (class_instances ci)
1006+ vsep (map (dumpInstance ist ctxt) (class_instances ci))
1005− iPrintResult ""
1006−
1007−dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
1007+ where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation
1008−dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
1008+ dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t
1009−
1010−dumpDefaultInstance :: PDecl -> Idris ()
1009+ dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation
1011−dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t
1010+ dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t
1012−
1011+ dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation
1013−dumpInstance :: Name -> Idris ()
1012+ dumpInstance ist ctxt n = vsep . map (\t -> pp ist (delab ist t)) $ lookupTy n ctxt
1014−dumpInstance n = do i <- getIState
1013+ pp ist = prettyImp (opt_showimp (idris_options ist))
1015− ctxt <- getContext
1016− case lookupTy n ctxt of
1017− ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts
1018
1014
1019showTotal :: Totality -> IState -> String
1015showTotal :: Totality -> IState -> String
1020showTotal t@(Partial (Other ns)) i
1016showTotal t@(Partial (Other ns)) i