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