Report Emacs bug: Quail input breaks delete-char behaviour

[Generic Isabelle user]

Step 1: In a theory file buffer, type a character like "-" or ".", which is an initial character in a Unicode shortcut sequence. The character displays with an underline, indicating this.

Step 2: Press "delete", intending to delete the chararacter to the right of the insertion point.

Result: The character that I just typed ("-" or ".") is deleted instead, as if I had pressed "backspace".

C-h k shows that "delete" is bound to unicode-tokens-delete-char, and "backspace" is bound to unicode-tokens-delete-backward-char. It appears that while entering a unicode token shortcut (when characters are shown with the underline) both of these do the same thing.

Versions: Isabelle Proof General, Version 4.1pre101216; GNU Emacs 23.2.1 (i686-pc-linux-gnu, GTK+ Version 2.21.6); Isabelle 2011; Ubuntu 10.10.

[David Aspinall]

Thanks for the bug report.

This looks to be a bug in the underlying Emacs functionality used by Unicode Tokens, the quail input mechanism.

You can see the same effect with:

1. switch to *scratch*
2. M-x set-input-method RET TeX RET
3. Type "xyz", C-a
4. Type "\alpha" (see alpha, verify TeX input method)
5. Type "\a" then DELETE.

Again at step 4, the delete is backward, not forward as expected.

[David Aspinall]

Reported upstream

[David Aspinall]

See here ​http://debbugs.gnu.org/cgi/bugreport.cgi?bug=9022

Unfortunately one of the Emacs maintainers jumped up immediately and declared this behaviour intentional because the rebinding is explicit in the code! It seems like an obvious error to me, causing needless confusion. I have tried to argue this...