[Agda] interactive mode

[Nils Anders Danielsson]

On 2011-01-28 22:17, Ramana Kumar wrote:
> It's 3 years old - was anything implemented?

No.

> If not, would anyone more experienced with Haskell and Agda like to
> help me decouple Agda from Emacs?

It would be great if someone could create a reusable interface between
the Agda backend and various kinds of frontends.

The current interface is implemented by the module
Agda.Interaction.GhciTop, which is used by the Emacs Lisp file
agda2-mode.el. You may want to study these files.

If you want to go ahead with this I think it would be good to start with
a description of what the interface should support. What other
frontend(s) do you have in mind? I think the main problem with the
current interface, as seen from the user perspective, is that the
current module needs to be reloaded far too often (after case-splits,
for instance, or if you want up-to-date colours after filling a goal).
It would be good if that could be avoided.

However, I suspect that the person implementing a new interface would
benefit from some hands-on knowledge of the old one, so you might have
to sacrifice your own Emacs innocence in order to maintain that of
others.

-- 
/NAD