10a5bd6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tidy up the IState when classes are undefined

commit10a5bd66d1371f3f4ca3698224f7a2161b452c06 authorAlyssa Carter <trillionalyssa@gmail.com> dateTue 5 Aug 2014, 16:15 (12 years ago) parenta37fc8a

2 files changed+6

unifiedsplit

src/Idris/ASTUtils.hs+3

@@ -142,6 +142,9 @@ known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation

142142known_terms = Field (definitions . tt_ctxt)

143143 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

144144

145+known_classes :: Field IState (Ctxt ClassInfo)

146+known_classes = Field idris_classes (\v state -> state {idris_classes = idris_classes state})

147+

145148

146149-- Names defined at the repl

147150----------------------------

src/Idris/REPL.hs+3

@@ -780,6 +780,9 @@ process fn (Undefine names) = undefine names

780780 else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")

781781 undefine' names already

782782 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

783786 fmodifyState repl_definitions (delete n)

784787 undefClosure n =

785788 do replDefs <- idris_repl_defs `fmap` get