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