[Agda] Agda and Emacs mode

[Andreas Abel]

s/agda-setup/agda-mode/

On 09.12.2014 19:59, Andrea Vezzosi wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/