@@ -691,6 +691,7 @@ process h fn (NewDefn decls) = do
691691 defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do
692692 elabDecl EAll recinfo tyDecl
693693 elabClauses recinfo fc opts name (concatMap getClauses decls)
694+ setReplDefined (Just name)
694695 defineName [PClauses fc opts _ [clause]] = do
695696 let pterm = getRHS clause
696697 (tm,ty) <- elabVal recinfo ERHS pterm
@@ -736,16 +737,33 @@ process h fn (Undefine names) = undefine names
736737 undefine :: [Name] -> Idris ()
737738 undefine [] = do
738739 allDefined <- idris_repl_defs `fmap` get
739− undefine' allDefined
740− undefine names = undefine' names
741− undefine' [] = return ()
742− undefine' (n:names) = do
740+ undefine' allDefined []
741+ -- Keep track of which names you've removed so you can
742+ -- print them out to the user afterward
743+ undefine names = undefine' names []
744+ undefine' [] list = do ihputStrLn h (show list)
745+ return ()
746+ undefine' (n:names) already = do
743747 allDefined <- idris_repl_defs `fmap` get
744748 if n `elem` allDefined
745− then fputState (ctxt_lookup n . known_terms) Nothing
746− else tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")
747− fmodifyState repl_definitions (delete n)
748− undefine' names
749+ then do undefinedJustNow <- undefClosure n
750+ undefine' names (undefinedJustNow ++ already)
751+ else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")
752+ undefine' names already
753+ undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing
754+ fmodifyState repl_definitions (delete n)
755+ undefClosure n =
756+ do replDefs <- idris_repl_defs `fmap` get
757+ callGraph <- whoCalls n
758+ let users' = case lookup n callGraph of
759+ Just ns -> ns
760+ Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)
761+ users = filter (`elem` replDefs) users'
762+ undefinedJustNow <- concat `fmap` mapM undefClosure users
763+ undefOne n
764+ return (n : undefinedJustNow)
765+
766+
749767
750768process h fn (ExecVal t)
751769 = do ctxt <- getContext