4d33a16 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixity declarations work in the repl now.

commit4d33a16e2a65de8412d022c0e59470ec5f45c996 authorAlyssa Carter <trillionalyssa@gmail.com> dateThu 24 Jul 2014, 15:52 (12 years ago) parentad81ad3

2 files changed+7−1

compare with master

unifiedsplit

src/Idris/ASTUtils.hs+4 src/Idris/REPL.hs+3−1

src/Idris/ASTUtils.hs+4

@@ -147,3 +147,7 @@ known_terms = Field (definitions . tt_ctxt)

147147----------------------------

148148repl_definitions :: Field IState [Name]

149149repl_definitions = Field idris_repl_defs (\v state -> state {idris_repl_defs = v})

150+

151+-- Fixity declarations in an IState

152+idris_fixities :: Field IState [FixDecl]

153+idris_fixities = Field idris_infixes (\v state -> state {idris_infixes = v})

src/Idris/REPL.hs+3−1

@@ -696,7 +696,9 @@ process h fn (NewDefn decls) = do

696696 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))

697697 setReplDefined (Just $ getClauseName clause)

698698 -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way

699− defineName (PFix{}:_) = tclift $ tfail (Msg "That kind of declaration is not supported. If you feel it should be supported, please submit an issue at https://github.com/idris-lang/Idris-dev.")

699+ defineName (PFix fc fixity strs : defns) = do

700+ fmodifyState idris_fixities (map (Fix fixity) strs ++)

701+ unless (null defns) $ defineName defns

700702 defineName (PSyntax{}:_) = tclift $ tfail (Msg "That kind of declaration is not supported. If you feel it should be supported, please submit an issue at https://github.com/idris-lang/Idris-dev.")

701703 defineName decls = do

702704 elabDecls toplevel decls