Search code examples
emacsproof-general

Emacs cursor jumps before period on Proof General


I only encounter this problem when running Proof General. I'm assuming this is some random minor mode that is started by Proof General, but can't figure out which one! I include a list of minor modes bellow, in case you can recognise the name.

If I place a period in Emacs, the cursor will jump before it, like so:

Writing something|

Writing something.|

Writing something|.

Where | represents cursor and the last two lined happen immediately one after the other.

the same happens if I click at the end of a line with a period. The cursor will appear after the period and immediately jump before the period.

Some sentence. (click here)

Some sentence. |

Some sentence|.

Where the last two lined happen immediately one after the other.

Here is the list of minor modes, in case you can spot the name:

Aquamacs-Autoface Auto-Composition
Auto-Compression Auto-Encryption Blink-Cursor Column-Number Cua
Delete-Selection Electric-Indent File-Name-Shadow Font-Lock
Global-Font-Lock Holes Line-Number Menu-Bar Mouse-Wheel Osx-Key
Recentf Savehist Show-Paren Smart-Frame-Positioning Tabbar
Tabbar-Mwheel Tool-Bar Tooltip Transient-Mark

key             binding
---             -------

^C              Prefix Command
ESC             Prefix Command
.               proof-electric-terminator
<C-M-down>      pg-move-region-down
<C-M-mouse-3>   proof-mouse-goto-point
<C-M-up>        pg-move-region-up
<C-S-mouse-1>   pg-identifier-under-mouse-query
<C-return>      proof-script-complete
  (that binding is currently shadowed by another mode)
<M-down>        proof-forward-command
<M-up>          proof-backward-command
<remap>         Prefix Command
... then a bunch of Proof specific minor modes...

Solution

  • Proof General is incompatible with show-paren-mode. You can turn it off with M-x show-paren-mode or by putting (add-hook 'proof-ready-for-assistant-hook (lambda () (show-paren-mode 0))) in the appropriate place in your .emacs.

    See http://proofgeneral.inf.ed.ac.uk/trac/ticket/496.