@@ -701,7 +701,7 @@ process h fn (NewDefn decls) = do
701 unless (null defns) $ defineName defns
701 unless (null defns) $ defineName defns
702 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.")
702 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.")
703 defineName decls = do
703 defineName decls = do
704− elabDecls toplevel decls
704+ elabDecls toplevel (map fixClauses decls)
705 setReplDefined (getName (head decls))
705 setReplDefined (getName (head decls))
706 getClauses (PClauses fc opts name clauses) = clauses
706 getClauses (PClauses fc opts name clauses) = clauses
707 getClauses _ = []
707 getClauses _ = []
@@ -715,6 +715,16 @@ process h fn (NewDefn decls) = do
715 setReplDefined (Just n) = do
715 setReplDefined (Just n) = do
716 oldState <- get
716 oldState <- get
717 fmodifyState repl_definitions (n:)
717 fmodifyState repl_definitions (n:)
718+ -- the "name" field of PClauses seems to always be MN 2 "__", so we need to
719+ -- retrieve the actual name from deeper inside.
720+ -- This should really be a full recursive walk through the structure of PDecl, but
721+ -- I think it should work this way and I want to test sooner. Also lazy.
722+ fixClauses :: PDecl' t -> PDecl' t
723+ fixClauses (PClauses fc opts _ css@(clause:cs)) =
724+ PClauses fc opts (getClauseName clause) css
725+ fixClauses (PInstance syn fc constraints cls parms ty instName decls) =
726+ PInstance syn fc constraints cls parms ty instName (map fixClauses decls)
727+ fixClauses decl = decl
719process h fn (Undefine names) = undefine names
729process h fn (Undefine names) = undefine names