[Agda] Emacs interface

[Wouter Swierstra]

> Perhaps what you have seen is an instance of this bug:
> http://code.google.com/p/agda/issues/detail?id=118.

That looks like it. Thanks for pointing this out.

>> 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.
>
> As Darin mentioned this problem should be less severe in the latest
> version.

I've updated my Agda and it seems to be quite a bit better. I'll try  
to keep track of any funny behaviour.

> Stefan Monnier wanted to be able to use syntax highlighting info when
> debugging type incorrect code. I find this reasonable. Perhaps we  
> should
> add some other indicator to show that the code is completely type
> correct. (A special background colour?)

I can see it's a bit controversial - it's nice to be able to browse  
code that hasn't been type-checked. I'd just like something that makes  
it blatantly obvious when code has been type checked succesfully, when  
their are unfulfilled constraints or functions that fail the  
termination checker, or when there is a type error.

>>  * make an implicit argument explicit and visa versa;

Select an implicit argument in the type signature, hit some emacs  
commands, and the argument gets made explicit (in the type signature)  
and an additional argument gets added on the left-hand side of the  
definitions. There's a similar operation to turn explicit arguments  
into implicit ones. At the moment, when I'm not sure which arguments  
can be left out, I tend to make things overly explicit and refine my  
definitions later. It be nice if there was a bit more support for this  
kind of development.

> Please document your feature requests on the bug tracker, so that we  
> do
> not forget them.

Done. Thanks for all the replies,

   Wouter