[Agda] New Agda-specific input method

Nils Anders Danielsson nils.anders.danielsson at gmail.com
Sat Jul 19 13:39:57 CEST 2008


Hi,

To avoid further complaints about the use of non-ASCII characters in
the standard library I have developed a new Emacs input method for
Agda. This input method is enabled by default in the Emacs mode.

The input method is highly configurable (using M-x customize-group
agda-input). You can import and tweak bindings from other Quail input
methods (but for technical reasons only for non-Latin-1 characters),
modify the default Agda-specific bindings, and add your own ones.

By default the input method is set up so that all bindings start with
"\"; this is easily changed. Most of the bindings from the TeX input
method are imported, and I have also added Agda-specific ones. The
default settings should make it possible to type all characters used
in the standard library, and many more. Use M-x
agda-input-show-translations to see the current bindings (except those
for Latin-1 characters).

Note that the Agda input method allows a binding to map to several
different characters. In that case you can choose between them using
the arrow or digit keys. (When you are in that situation you can type
C-h for a list of some other potentially useful key bindings.)

The default bindings have only been tested for a week or two, and
might change in the future. Feedback is welcome.

By the way, I considered using abbrevs instead of an input method.
However, I did not find any way to expand abbrevs in the minibuffer,
so I abandoned that idea.

-- 
/NAD


More information about the Agda mailing list