[Agda] Agda and Emacs mode

[Mateusz Kowalczyk]

On 12/10/2014 12:37 AM, Mateusz Kowalczyk wrote:
> On 12/09/2014 11:27 AM, Andrej Bauer 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
>>
> 
> Some investigation was done
> 

Apologies, didn't mean to send that, damn Thunderbird.

What I was going to say is that there was some investigation done into
these commands by previous project (for the Atom editor I believe) but I
can't find the file now. I started to do ‘the emacs way’ of talking to
the process in Yi but it's very quickly becoming cumbersome. If your
student is going to use Haskell, I recommend he does what Andreas
recommended to me some weeks ago: collect the functions we want Agda to
expose and try to establish an API proper, maintaining it between Agda
releases.

-- 
Mateusz K.