[Agda] Emacs interface

[Nils Anders Danielsson]

On 2009-04-05 19:03, Wouter Swierstra wrote:
> 
> 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?

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

> 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.

If you want Emacs to remove all trailing white space from Agda files
before saving, then you can add the following code to your .emacs:

(add-hook 'agda2-mode-hook
          '(lambda nil
             (add-hook 'write-contents-hooks
                       (lambda nil
                         (if (not buffer-read-only)
                             (delete-trailing-whitespace))))))

Note that this can be problematic if you are collaborating with people
who do not use this setting (because of noise in patches).

> 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.

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 find this to be a small issue,
though, so if you want it you may have to implement it yourself.

>   * make an implicit argument explicit and visa versa;

Can you explain in more detail what you have in mind?

>   * have a command to let Agda refine a goal automatically if there is 
> only one constructor possible.

C-c C-s (/s/olve) often works.

> I hope these comments and suggestions are helpful.

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

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.