@@ -1183,19 +1183,20 @@ process fn (MakeDoc s) =
11831183process fn (PrintDef n) =
11841184 do ist <- getIState
11851185 ctxt <- getContext
1186− let patdefs = idris_patdefs ist
1186+ let ambiguous = length (lookupNames n ctxt) > 1
1187+ patdefs = idris_patdefs ist
11871188 tyinfo = idris_datatypes ist
1188− result = map (ppDef ist) (lookupCtxtName n patdefs) ++
1189− map (ppTy ist) (lookupCtxtName n tyinfo) ++
1190− map (ppCon ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1189+ result = map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
1190+ map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
1191+ map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
11911192 case result of
11921193 [] -> iPrintError "Not found"
1193− outs -> iRenderResult . vsep $ outs
1194− where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1195− ppDef ist (n, (clauses, missing)) =
1196− prettyName True True [] n <+> colon <+>
1194+ outs -> iRenderResult . vsep . punctuate line $ outs
1195+ where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1196+ ppDef amb ist (n, (clauses, missing)) =
1197+ prettyName True amb [] n <+> colon <+>
11971198 align (pprintDelabTy ist n) <$>
1198− indent 2 (ppClauses ist clauses <> ppMissing missing)
1199+ ppClauses ist clauses <> ppMissing missing
11991200 ppClauses ist [] = text "No clauses."
12001201 ppClauses ist cs = vsep (map pp cs)
12011202 where pp (vars, lhs, rhs) =
@@ -1208,16 +1209,16 @@ process fn (PrintDef n) =
12081209 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
12091210 ppMissing _ = empty
12101211
1211− ppTy :: IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1212− ppTy ist (n, TI constructors isCodata _ _ _)
1213− = kwd key <+> prettyName True True [] n <+> colon <+>
1212+ ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1213+ ppTy amb ist (n, TI constructors isCodata _ _ _)
1214+ = kwd key <+> prettyName True amb [] n <+> colon <+>
12141215 align (pprintDelabTy ist n) <+> kwd "where" <$>
1215− indent 2 (vsep (map (ppCon ist) constructors))
1216+ indent 2 (vsep (map (ppCon False ist) constructors))
12161217 where
12171218 key | isCodata = "codata"
12181219 | otherwise = "data"
12191220 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)
12211222
12221223showTotal :: Totality -> IState -> String
12231224showTotal t@(Partial (Other ns)) i