[Agda] Spanish keyboard + Agda input-mode

[Nils Anders Danielsson]

On 2014-04-23 20:51, Michael Shulman wrote:
> I have a student who is trying to install Agda on his Mac (using
> Aquamacs).  However, his computer (like himself) is from Spain, and
> lacks a backslash key.  There is a key combination which lets him type
> a backslash character, but it doesn't drop him into the agda
> input-mode for typing unicode characters; it just prints a backslash.
> I don't understand enough about how *macs input-modes work to fix it;
> there doesn't seem to be an elisp function that I can bind to another
> key.  Any suggestions?

One option is to change the prefix character from backslash to something
else. Type

   M-x customize-group RET agda-input RET,

and modify the setting called "Agda Input Tweak All" in a suitable way.

Another option is to change the keyboard mapping using the operating
system. For instance, I have mapped backslash to an easily accessible
key on my keyboard. However, I don't know how or if that can be done
using MacOS.

-- 
/NAD