Adding a prettyprinted message for undefining names
commita37fc8a44fe539b0a27a1ffdb77fa5acd32f4454
authorAlyssa Carter <trillionalyssa@gmail.com>
dateTue 5 Aug 2014, 16:02 (12 years ago)
parentecea9ad
src/Idris/Output.hs+6
@@ -164,3 +164,9 @@ warnTotality :: Idris ()
164164warnTotality = do ist <- getIState
165165 mapM_ (warn ist) (nub (idris_totcheckfail ist))
166166 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
770770 -- Keep track of which names you've removed so you can
771771 -- print them out to the user afterward
772772 undefine names = undefine' names []
773− undefine' [] list = do iputStrLn (show list)
773+ undefine' [] list = do iRenderOutput $ printUndefinedNames list
774774 return ()
775775 undefine' (n:names) already = do
776776 allDefined <- idris_repl_defs `fmap` get