[Agda] Abbreviation mode
Robin Green
greenrd at greenrd.org
Fri Oct 2 16:38:04 CEST 2009
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.
Also, the "Agda2 Mode Abbrevs Use Defaults:" option should probably
default to No.
How does one use the default abbreviations if that option is turned
off, by the way?
--
Robin
More information about the Agda
mailing list