[Agda] Abbreviation mode
Anton Setzer
A.G.Setzer at swansea.ac.uk
Fri Oct 2 18:58:09 CEST 2009
Robin Green wrote:
> Two points about abbrev-mode:
>
> The instructions on the wiki at
> http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Abbreviation
> don't work - the ' and " characters have been turned into so-called
> "Smart Quotes", which confuses emacs.
>
>
I don't understand the problem. For me the abbreviation mode works well.
All you need to be aware of is that you need a space like character
before the abbreviation and one after it in order for it to expand. I don't
know exactly which characters are space like or not, space itself
definitely is.
> Also, the "Agda2 Mode Abbrevs Use Defaults:" option should probably
> default to No.
>
>
The defaults are very extreme, expanding for instance an 'm' to
I think module, which makes it impossible to use any variables.
> How does one use the default abbreviations if that option is turned
> off, by the way?
>
>
You can run it once with the default set on, then edit abbreviations,
and look for the abbreviations added, copy them to a file.
Then turn the defaults off, and add those you want to the abbreviation file
and activate the abbreviations by I think C-c C-c
Anton
--
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK
Telephone:
(national) (01792) 513368
(international) +44 1792 513368
Fax:
(national) (01792) 295708
(international) +44 1792 295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
More information about the Agda
mailing list