git.iko.soy/Idris-dev
on master help sign in
Minor rewording of error message
7dca9b4Edwin Brady
src/Idris/Delaborate.hs+3−3
compare with master
unifiedsplit
@@ -346,19 +346,19 @@ pprintErr' i (AlreadyDefined n) = annName n<+>
346pprintErr' i (ProofSearchFail e) = pprintErr' i e
346pprintErr' i (ProofSearchFail e) = pprintErr' i e
347pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delab i tm))
347pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delab i tm))
348pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
348pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
349−pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
349+pprintErr' i (Elaborating s n e) = text "When checking" <+> text s <>
350 annName' n (showqual i n) <> colon <$>
350 annName' n (showqual i n) <> colon <$>
351 pprintErr' i e
351 pprintErr' i e
352pprintErr' i (ElaboratingArg f x _ e)
352pprintErr' i (ElaboratingArg f x _ e)
353 | isInternal f = pprintErr' i e
353 | isInternal f = pprintErr' i e
354 | isUN x =
354 | isUN x =
355− text "When elaborating argument" <+>
355+ text "When checking argument" <+>
356 annotate (AnnBoundName x False) (text (showbasic x)) <+> -- TODO check plicity
356 annotate (AnnBoundName x False) (text (showbasic x)) <+> -- TODO check plicity
357 -- Issue #1591 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1591
357 -- Issue #1591 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1591
358 text "to" <+> whatIsName <> annName f <> colon <>
358 text "to" <+> whatIsName <> annName f <> colon <>
359 indented (pprintErr' i e)
359 indented (pprintErr' i e)
360 | otherwise =
360 | otherwise =
361− text "When elaborating an application of" <+> whatIsName <>
361+ text "When checking an application of" <+> whatIsName <>
362 annName f <> colon <> indented (pprintErr' i e)
362 annName f <> colon <> indented (pprintErr' i e)
363 where whatIsName = let ctxt = tt_ctxt i
363 where whatIsName = let ctxt = tt_ctxt i
364 in if isTConName f ctxt
364 in if isTConName f ctxt
src/Idris/Interactive.hs+1−1
@@ -162,7 +162,7 @@ makeWith fn updatefile l n
162doProofSearch :: FilePath -> Bool -> Bool ->
162doProofSearch :: FilePath -> Bool -> Bool ->
163 Int -> Name -> [Name] -> Maybe Int -> Idris ()
163 Int -> Name -> [Name] -> Maybe Int -> Idris ()
164doProofSearch fn updatefile rec l n hints Nothing
164doProofSearch fn updatefile rec l n hints Nothing
165− = doProofSearch fn updatefile rec l n hints (Just 10)
165+ = doProofSearch fn updatefile rec l n hints (Just 20)
166doProofSearch fn updatefile rec l n hints (Just depth)
166doProofSearch fn updatefile rec l n hints (Just depth)
167 = do src <- runIO $ readSource fn
167 = do src <- runIO $ readSource fn
168 let (before, tyline : later) = splitAt (l-1) (lines src)
168 let (before, tyline : later) = splitAt (l-1) (lines src)