git.iko.soy/Idris-dev
on master help sign in
Adding a prettyprinted message for undefining names
a37fc8aAlyssa Carter
src/Idris/Output.hs+6
compare with master
unifiedsplit
@@ -164,3 +164,9 @@ warnTotality :: Idris ()
164warnTotality = do ist <- getIState
164warnTotality = do ist <- getIState
165 mapM_ (warn ist) (nub (idris_totcheckfail ist))
165 mapM_ (warn ist) (nub (idris_totcheckfail ist))
166 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
166 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))
167+
168+
169+printUndefinedNames :: [Name] -> Doc OutputAnnotation
170+printUndefinedNames ns = text "Undefined " <> names <> text "."
171+ where names = encloseSep empty empty (char ',') $ map ppName ns
172+ ppName = prettyName True True []
src/Idris/REPL.hs+1−1
@@ -770,7 +770,7 @@ process fn (Undefine names) = undefine names
770 -- Keep track of which names you've removed so you can
770 -- Keep track of which names you've removed so you can
771 -- print them out to the user afterward
771 -- print them out to the user afterward
772 undefine names = undefine' names []
772 undefine names = undefine' names []
773− undefine' [] list = do iputStrLn (show list)
773+ undefine' [] list = do iRenderOutput $ printUndefinedNames list
774 return ()
774 return ()
775 undefine' (n:names) already = do
775 undefine' (n:names) already = do
776 allDefined <- idris_repl_defs `fmap` get
776 allDefined <- idris_repl_defs `fmap` get