Are there any documents describing how agda2-mode is implemented? I
found the interactive goals (in the form { }0) used in agda2-mode are
very useful and want to have such mechanism for other purposes, too.
Do I have to read the emacs lisp files? Thanks in advance.
Sincerely,
--
Kenichi Asai