[Agda] Emacs interface

[Wouter Swierstra]

I've been using Agda a bit recently. Although the emacs interface is  
very nice, there's a few things I'd still like to see improved. I  
thought I'd better publicly document some of my suggestions - hence  
this e-mail.

First of all, I seem to be able to construct terms by iteratively  
refining goals that, when I reload the file, don't type check. I don't  
have an example at hand. Is this a known issue?

A more minor issue: there are sometimes some spurious spaces left  
lying about after refining a goal. It'd be nice if this could be  
avoided.

I remember that a file used to be syntax highlighted only if it type  
checked. Nowadays, any file is highlighted, provided the syntax  
highlighting information is available. I actually may prefer the old  
situation: it makes it very clear when a file has been loaded and  
checked, and when it hasn't.

It would also be nice to customise the name generation when case  
splitting. I tend to avoid using C-c C-c because the generated names  
are really horrible. Should there be a pragma for this?

And finally, here's a few things I find myself doing by hand that  
could be automated:
   * make an implicit argument explicit and visa versa;
   * convert selected area to goal (i.e. mark with {! ... !});
   * have a command to let Agda refine a goal automatically if there  
is only one constructor possible.

I hope these comments and suggestions are helpful. All the best,

   Wouter