[Agda] Agda and Emacs mode

[Andrea Vezzosi]

There is some documentation on the commands agda --interaction accepts:

https://github.com/agda/agda/blob/master/src/full/Agda/Interaction/InteractionTop.hs#L285

The concrete syntax should be easy to figure out by looking at the
emacs buffer *agda2* during/after an agda session.

The responses are printed out as s-expressions, which should make them
easy to parse in general.
Patching agda to optionally produce the output in some other format
shouldn't be hard either, it's a matter of writing a different pretty
printer for the Response type:
https://github.com/agda/agda/blob/master/src/full/Agda/Interaction/Response.hs#L37

So overall it needs some amount of reverse engineering but not too bad?

Only agda-setup should require an emacs installation, its job is to
setup the emacs mode though.

Cheers,
Andrea

On Tue, Dec 9, 2014 at 12:27 PM, Andrej Bauer <andrej.bauer at andrej.com> wrote:
> I have a master's student who would like to write a GUI for Agda on
> OSX (well, was told to do so).
>
> I suggested that he should just hook into Agda's communication with
> Emacs. Is there reasonable documentation on how Agda communicates with
> Emacs?
>
> Also, he now tells me that the Agda executable presupposes the
> existence of Emacs, which I have a hard time believing.
>
> Can someone shed some light on how realistic a project this is?
>
> With kind regards,
>
> Andrej
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda