@@ -1183,19 +1183,20 @@ process fn (MakeDoc s) =
1183process fn (PrintDef n) =
1183process fn (PrintDef n) =
1184 do ist <- getIState
1184 do ist <- getIState
1185 ctxt <- getContext
1185 ctxt <- getContext
1186+ let ambiguous = length (lookupNames n ctxt) > 1
1186− let patdefs = idris_patdefs ist
1187+ patdefs = idris_patdefs ist
1187 tyinfo = idris_datatypes ist
1188 tyinfo = idris_datatypes ist
1188− result = map (ppDef ist) (lookupCtxtName n patdefs) ++
1189+ result = map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
1189− map (ppTy ist) (lookupCtxtName n tyinfo) ++
1190+ map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
1190− map (ppCon ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1191+ map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1191 case result of
1192 case result of
1192 [] -> iPrintError "Not found"
1193 [] -> iPrintError "Not found"
1193− outs -> iRenderResult . vsep $ outs
1194+ outs -> iRenderResult . vsep . punctuate line $ outs
1194− where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1195+ where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1195− ppDef ist (n, (clauses, missing)) =
1196+ ppDef amb ist (n, (clauses, missing)) =
1196− prettyName True True [] n <+> colon <+>
1197+ prettyName True amb [] n <+> colon <+>
1197 align (pprintDelabTy ist n) <$>
1198 align (pprintDelabTy ist n) <$>
1198− indent 2 (ppClauses ist clauses <> ppMissing missing)
1199+ ppClauses ist clauses <> ppMissing missing
1199 ppClauses ist [] = text "No clauses."
1200 ppClauses ist [] = text "No clauses."
1200 ppClauses ist cs = vsep (map pp cs)
1201 ppClauses ist cs = vsep (map pp cs)
1201 where pp (vars, lhs, rhs) =
1202 where pp (vars, lhs, rhs) =
@@ -1208,16 +1209,16 @@ process fn (PrintDef n) =
1208 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1209 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1209 ppMissing _ = empty
1210 ppMissing _ = empty
1211− ppTy :: IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1212+ ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1212− ppTy ist (n, TI constructors isCodata _ _ _)
1213+ ppTy amb ist (n, TI constructors isCodata _ _ _)
1213− = kwd key <+> prettyName True True [] n <+> colon <+>
1214+ = kwd key <+> prettyName True amb [] n <+> colon <+>
1214 align (pprintDelabTy ist n) <+> kwd "where" <$>
1215 align (pprintDelabTy ist n) <+> kwd "where" <$>
1215− indent 2 (vsep (map (ppCon ist) constructors))
1216+ indent 2 (vsep (map (ppCon False ist) constructors))
1217 key | isCodata = "codata"
1218 key | isCodata = "codata"
1218 | otherwise = "data"
1219 | otherwise = "data"
1219 kwd = annotate AnnKeyword . text
1220 kwd = annotate AnnKeyword . text
1220− ppCon ist n = prettyName True False [] n <+> colon <+> align (pprintDelabTy ist n)
1221+ ppCon amb ist n = prettyName True amb [] n <+> colon <+> align (pprintDelabTy ist n)
1222showTotal :: Totality -> IState -> String
1223showTotal :: Totality -> IState -> String
1223showTotal t@(Partial (Other ns)) i
1224showTotal t@(Partial (Other ns)) i