@@ -1172,10 +1172,12 @@ process fn (MakeDoc s) =
1172 Left err -> iPrintError err
1172 Left err -> iPrintError err
1173process fn (PrintDef n) =
1173process fn (PrintDef n) =
1174 do ist <- getIState
1174 do ist <- getIState
1175 let patdefs = idris_patdefs ist
1176 let patdefs = idris_patdefs ist
1176 tyinfo = idris_datatypes ist
1177 tyinfo = idris_datatypes ist
1177 result = map (ppDef ist) (lookupCtxtName n patdefs) ++
1178 result = map (ppDef ist) (lookupCtxtName n patdefs) ++
1178− map (ppTy ist) (lookupCtxtName n tyinfo)
1179+ map (ppTy ist) (lookupCtxtName n tyinfo) ++
1180+ map (ppCon ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1179 case result of
1181 case result of
1180 [] -> iPrintError "Not found"
1182 [] -> iPrintError "Not found"
1181 outs -> iRenderResult . vsep $ outs
1183 outs -> iRenderResult . vsep $ outs
@@ -1205,7 +1207,7 @@ process fn (PrintDef n) =
1205 key | isCodata = "codata"
1207 key | isCodata = "codata"
1206 | otherwise = "data"
1208 | otherwise = "data"
1207 kwd = annotate AnnKeyword . text
1209 kwd = annotate AnnKeyword . text
1208− ppCon ist n = prettyName True False [] n <+> colon <+> align (pprintDelabTy ist n)
1210+ ppCon ist n = prettyName True False [] n <+> colon <+> align (pprintDelabTy ist n)
1210showTotal :: Totality -> IState -> String
1212showTotal :: Totality -> IState -> String
1211showTotal t@(Partial (Other ns)) i
1213showTotal t@(Partial (Other ns)) i