git.iko.soy/Idris-dev
on master help sign in
Highlight variables from error context as bound
f7b466dDavid Raymond Christiansen
src/Idris/Delaborate.hs+15−8
compare with master
unifiedsplit
@@ -127,7 +127,10 @@ indented :: Doc a -> Doc a
127indented = nest errorIndent . (line <>)
127indented = nest errorIndent . (line <>)
128
128
129pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
129pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
130+pprintTerm ist = pprintTerm' ist []
131+
132+pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
130−pprintTerm ist = prettyImp (opt_showimp (idris_options ist))
133+pprintTerm' ist = pprintPTerm (opt_showimp (idris_options ist))
131
134
132pshow :: IState -> Err -> String
135pshow :: IState -> Err -> String
133pshow ist err = displayDecorated (consoleDecorate ist) .
136pshow ist err = displayDecorated (consoleDecorate ist) .
@@ -144,23 +147,26 @@ pprintErr' i (InternalMsg s) =
144 text ("Please consider reporting at " ++ bugaddr)
147 text ("Please consider reporting at " ++ bugaddr)
145 ]
148 ]
146pprintErr' i (CantUnify _ x y e sc s) =
149pprintErr' i (CantUnify _ x y e sc s) =
147− text "Can't unify" <> indented (pprintTerm i (delab i x)) <$>
150+ text "Can't unify" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x)) <$>
148− text "with" <> indented (pprintTerm i (delab i y)) <>
151+ text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y)) <>
149 case e of
152 case e of
150 Msg "" -> empty
153 Msg "" -> empty
151 _ -> line <> line <> text "Specifically:" <>
154 _ -> line <> line <> text "Specifically:" <>
152 indented (pprintErr' i e) <>
155 indented (pprintErr' i e) <>
153 if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
156 if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
154pprintErr' i (CantConvert x y env) =
157pprintErr' i (CantConvert x y env) =
158+ text "Can't convert" <>
155− text "Can't convert" <> indented (pprintTerm i (delab i x)) <$>
159+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>
160+ text "with" <>
156− text "with" <> indented (pprintTerm i (delab i y)) <>
161+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y)) <>
157 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
162 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
158pprintErr' i (CantSolveGoal x env) =
163pprintErr' i (CantSolveGoal x env) =
164+ text "Can't solve goal " <>
159− text "Can't solve goal " <> indented (pprintTerm i (delab i x)) <>
165+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <>
160 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
166 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
161pprintErr' i (UnifyScope n out tm env) =
167pprintErr' i (UnifyScope n out tm env) =
162 text "Can't unify" <> indented (annName n) <+>
168 text "Can't unify" <> indented (annName n) <+>
163− text "with" <> indented (pprintTerm i (delab i tm)) <+>
169+ text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
164 text "as" <> indented (annName out) <> text "is not in scope" <>
170 text "as" <> indented (annName out) <> text "is not in scope" <>
165 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
171 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
166pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
172pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
@@ -176,7 +182,8 @@ pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
176pprintErr' i (CantIntroduce ty) =
182pprintErr' i (CantIntroduce ty) =
177 text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)
183 text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)
178pprintErr' i (InfiniteUnify x tm env) =
184pprintErr' i (InfiniteUnify x tm env) =
179− text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>
185+ text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
186+ pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>
180 text "would lead to infinite value" <>
187 text "would lead to infinite value" <>
181 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
188 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
182pprintErr' i (NotInjective p x y) =
189pprintErr' i (NotInjective p x y) =