55ffc21 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1656,7 +1656,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1656 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

1657 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

1658 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)

1659− | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs

1659+ | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs

1660 || ppopt_pinames ppo && uname n =

1661 depth d . bracket p startPrec . group $

1662 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

src/Idris/Delaborate.hs+12

@@ -359,9 +359,21 @@ pprintErr' i (IncompleteTerm t)

359 (map pprintIncomplete (nub $ getMissing [] [] t))))

360 where

361 pprintIncomplete (tm, arg)

362+ | expname arg

363+ = text "Can't infer explicit argument to" <+>

364+ annTm tm (pprintTerm i (delabSugared i tm))

365+ | otherwise

362 = text "Can't infer argument" <+> annName arg <+> text "to" <+>

366 = text "Can't infer argument" <+> annName arg <+> text "to" <+>

363 annTm tm (pprintTerm i (delabSugared i tm))

367 annTm tm (pprintTerm i (delabSugared i tm))

364

368

369+ expname (UN n) = case str n of

370+ ('_':_) -> True

371+ _ -> False

372+ expname (MN _ n) = case str n of

373+ ('_':_) -> True

374+ _ -> False

375+ expname _ = False

376+

365 getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]

377 getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]

366 getMissing hs env (Bind n (Hole ty) sc)

378 getMissing hs env (Bind n (Hole ty) sc)

367 = getMissing (n : hs) (n : env) sc

379 = getMissing (n : hs) (n : env) sc

src/Idris/Interactive.hs+1−1

@@ -170,7 +170,7 @@ makeCase fn updatefile l n

170 do let fb = fn ++ "~"

171 runIO $ writeSource fb (unlines (before ++ newcase ++ later))

172 runIO $ copyFile fb fn

173− else iPrintResult (showSep "\n" newcase)

173+ else iPrintResult (showSep "\n" newcase ++"\n")

174 where addCaseSkel n line =

175 let b = brackets False line in

176 case findSubstr ('?':n) line of

src/Idris/ProofSearch.hs+1−1

@@ -321,7 +321,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

321 isImp (PImp p _ _ _ _) = (True, p)

322 isImp arg = (False, priority arg)

323

324−-- In interactive mode, only search for things if there is some constructor

324+-- In interactive mode, only search for things if there is some

325-- index to help pick a relevant constructor

326checkConstructor :: IState -> [Name] -> ElabD ()

327checkConstructor ist [] = return ()