[Agda] documents on the implementation of agda2-mode?

[Nils Anders Danielsson]

On 2015-05-13 09:38, Kenichi Asai wrote:
> Are there any documents describing how agda2-mode is implemented?

I don't think so.

> Do I have to read the emacs lisp files?

The basic idea is to do most processing in the Haskell library. The
Haskell backend and the Emacs frontend communicate via an API loosely
defined by Agda.Interaction.InteractionTop.Interaction and
Agda.Interaction.Response.Response:

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

Feel free to ask for more information.

-- 
/NAD