[Agda] Abbreviation mode

[Nils Anders Danielsson]

On 2009-10-02 15:38, Robin Green wrote:
> Also, the "Agda2 Mode Abbrevs Use Defaults:" option should probably
> default to No.

This seems like a good idea, I don't think these abbreviations are
widely used. They are not designed to be used with Abbrev mode, but
rather to be expanded manually using C-x '. I have changed the default
in the development version of Agda.

> How does one use the default abbreviations if that option is turned
> off, by the way?

By turning it on again? I don't understand the question.

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