Aquamacs point moving

[coquser]

When using Proof General for Coq in Aquamacs 3.0 (Emacs24.3.50.2), the point moves around unpredictably. It seems usually to happen when I type a full stop (electric terminator is off), but not always; I haven't been able to figure out just when. In this case, it moves back one character, so to right before the full stop. It also sometimes happens when I try to use the arrow keys to return the point to where it ought to be.

When it happens, I get "Error running timer `show-paren-function': (wrong-type-argument characterp nil)" in the minibuffer.

Anyway, this makes Proof General very difficult to use. A similar problem was reported (not by me) to Aquamacs at: ​http://emacs.1067599.n5.nabble.com/aquamacs-devel-Re-24-3-50-td314309.html, but with no solution in sight there. Any help is much appreciated!

[coquser]

This results from a conflict with show-paren-mode. Disabling show-paren-mode fixes the problem. You can add the following hook to disable show-paren-mode when using PG:

(add-hook 'proof-ready-for-assistant-hook (lambda () (show-paren-mode 0)))

[courtieu]

I would be interested in knowing if this still happens? P.

[coquser]

I am getting this same behavior right now in GNU Emacs 24.5.1 on Linux. So it is probably an incompatibility with the new behavior of show-paren-mode in Emacs24, not anything specific to Aquamacs.