[Agda] Abbreviation mode

[Nils Anders Danielsson]

On 2009-10-02 17:58, Anton Setzer wrote:
> The defaults are very extreme, expanding for instance an 'm' to
> I think module, which makes it impossible to use any variables.

The documentation states that "The abbrevs are designed to be expanded
explicitly, so users of `abbrev-mode' probably do not want to include
them". I find it quite useful to be able to type d C-x ' and get

  data  : Set where

inserted into the buffer, with the cursor between "data" and ":". This
behaviour should probably never have been the default, though.

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