@@ -98,35 +98,40 @@ pshow i (Msg s) = s
98pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
98pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
99 "\nThis is probably a bug, or a missing error message.\n" ++
99 "\nThis is probably a bug, or a missing error message.\n" ++
100 "Please consider reporting at " ++ bugaddr
100 "Please consider reporting at " ++ bugaddr
101−pshow i (CantUnify _ x y e sc s)
101+pshow i (CantUnify _ x y e sc s)
102 = let imps = opt_showimp (idris_options i) in
102 = let imps = opt_showimp (idris_options i) in
103+ let colour = idris_colourRepl i in
103− "Can't unify " ++ showImp Nothing imps False (delab i x)
104+ "Can't unify " ++ showImp (Just i) imps colour (delab i x)
104− ++ " with " ++ showImp Nothing imps False (delab i y) ++
105+ ++ " with " ++ showImp (Just i) imps colour (delab i y) ++
105-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
106-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
106 case e of
107 case e of
107 Msg "" -> ""
108 Msg "" -> ""
108− _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++
109+ _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++
109 if (opt_errContext (idris_options i)) then showSc i sc else ""
110 if (opt_errContext (idris_options i)) then showSc i sc else ""
110−pshow i (CantConvert x y env)
111+pshow i (CantConvert x y env)
111 = let imps = opt_showimp (idris_options i) in
112 = let imps = opt_showimp (idris_options i) in
113+ let colour = idris_colourRepl i in
112− "Can't convert " ++ showImp Nothing imps False (delab i x) ++ " with "
114+ "Can't convert " ++ showImp (Just i) imps colour (delab i x) ++ " with "
113− ++ showImp Nothing imps False (delab i y) ++
115+ ++ showImp (Just i) imps colour (delab i y) ++
114 if (opt_errContext (idris_options i)) then showSc i env else ""
116 if (opt_errContext (idris_options i)) then showSc i env else ""
115−pshow i (UnifyScope n out tm env)
117+pshow i (UnifyScope n out tm env)
116 = let imps = opt_showimp (idris_options i) in
118 = let imps = opt_showimp (idris_options i) in
119+ let colour = idris_colourRepl i in
117− "Can't unify " ++ show n ++ " with "
120+ "Can't unify " ++ show n ++ " with "
118− ++ showImp Nothing imps False (delab i tm) ++ " as " ++ show out ++
121+ ++ showImp (Just i) imps colour (delab i tm) ++ " as " ++ show out ++
119 " is not in scope" ++
122 " is not in scope" ++
120 if (opt_errContext (idris_options i)) then showSc i env else ""
123 if (opt_errContext (idris_options i)) then showSc i env else ""
121pshow i (CantInferType t)
124pshow i (CantInferType t)
122 = "Can't infer type for " ++ t
125 = "Can't infer type for " ++ t
123pshow i (NonFunctionType f ty)
126pshow i (NonFunctionType f ty)
124 = let imps = opt_showimp (idris_options i) in
127 = let imps = opt_showimp (idris_options i) in
128+ let colour = idris_colourRepl i in
125− showImp Nothing imps False (delab i f) ++ " does not have a function type ("
129+ showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
126− ++ showImp Nothing imps False (delab i ty) ++ ")"
130+ ++ showImp (Just i) imps colour (delab i ty) ++ ")"
127pshow i (CantIntroduce ty)
131pshow i (CantIntroduce ty)
128 = let imps = opt_showimp (idris_options i) in
132 = let imps = opt_showimp (idris_options i) in
133+ let colour = idris_colourRepl i in
129− "Can't use lambda here: type is " ++ showImp Nothing imps False (delab i ty)
134+ "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
130pshow i (InfiniteUnify x tm env)
135pshow i (InfiniteUnify x tm env)
131 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
136 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
132 " would lead to infinite value" ++
137 " would lead to infinite value" ++