git.iko.soy/Idris-dev
on master help sign in
Tidy up the IState when classes are undefined
10a5bd6Alyssa Carter
src/Idris/ASTUtils.hs+3
compare with master
unifiedsplit
@@ -142,6 +142,9 @@ known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation
142known_terms = Field (definitions . tt_ctxt)
142known_terms = Field (definitions . tt_ctxt)
143 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})
143 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})
144
144
145+known_classes :: Field IState (Ctxt ClassInfo)
146+known_classes = Field idris_classes (\v state -> state {idris_classes = idris_classes state})
147+
145
148
146-- Names defined at the repl
149-- Names defined at the repl
147----------------------------
150----------------------------
src/Idris/REPL.hs+3
@@ -780,6 +780,9 @@ process fn (Undefine names) = undefine names
780 else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")
780 else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")
781 undefine' names already
781 undefine' names already
782 undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing
782 undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing
783+ -- for now just assume it's a class. Eventually we'll want some kind of
784+ -- smart detection of exactly what kind of name we're undefining.
785+ fputState (ctxt_lookup n . known_classes) Nothing
783 fmodifyState repl_definitions (delete n)
786 fmodifyState repl_definitions (delete n)
784 undefClosure n =
787 undefClosure n =
785 do replDefs <- idris_repl_defs `fmap` get
788 do replDefs <- idris_repl_defs `fmap` get