@@ -13,7 +13,7 @@ import Idris.ErrReverse
1313import Idris.Delaborate
1414import Idris.Docstrings (Docstring, overview, renderDocstring)
1515import Idris.Prover
16−import Idris.Parser
16+import Idris.Parser hiding (indent)
1717import Idris.Primitives
1818import Idris.Coverage
1919import Idris.UnusedArgs
@@ -615,7 +615,8 @@ process h fn (DebugInfo n)
615615process h fn (Info n)
616616 = do i <- getIState
617617 case lookupCtxt n (idris_classes i) of
618− [c] -> classInfo c
618+ [c] -> do info <- classInfo c
619+ ihRenderResult h info
619620 _ -> iPrintError "Not a class"
620621process h fn (Search t) = iPrintError "Not implemented"
621622-- FIXME: There is far too much repetition in the cases below!
@@ -991,28 +992,30 @@ process h fn (Apropos a) =
991992 isUN (NS n _) = isUN n
992993 isUN _ = False
993994
994−classInfo :: ClassInfo -> Idris ()
995−classInfo ci = do iputStrLn "Methods:\n"
996− mapM_ dumpMethod (class_methods ci)
997− iputStrLn ""
998− iputStrLn "Default superclass instances:\n"
999− mapM_ dumpDefaultInstance (class_default_superclasses ci)
1000− iputStrLn ""
1001− iputStrLn "Instances:\n"
1002− mapM_ dumpInstance (class_instances ci)
1003− iPrintResult ""
1004−
1005−dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
1006−dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
1007−
1008−dumpDefaultInstance :: PDecl -> Idris ()
1009−dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t
1010−
1011−dumpInstance :: Name -> Idris ()
1012−dumpInstance n = do i <- getIState
1013− ctxt <- getContext
1014− case lookupTy n ctxt of
1015− ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts
995+classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)
996+classInfo ci = do ist <- getIState
997+ ctxt <- getContext
998+ return $
999+ text "Parameters:" <+>
1000+ hsep (punctuate comma (map (prettyName False params') params)) <>
1001+ line <> line <>
1002+ text "Methods:" <> line <>
1003+ indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>
1004+ text "Default superclass instances:" <>
1005+ line <>
1006+ indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>
1007+ line <>
1008+ text "Instances:" <> line <>
1009+ indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))
1010+ where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation
1011+ dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t
1012+ dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation
1013+ dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t
1014+ dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation
1015+ dumpInstance ist ctxt n = pp ist $ delabTy ist n
1016+ params = class_params ci
1017+ params' = zip params (repeat False)
1018+ pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []
10161019
10171020showTotal :: Totality -> IState -> String
10181021showTotal t@(Partial (Other ns)) i