Emacs游标在证据一般情况下跳过句号

Question

我只遇到这个问题时运行证明将军。我假设这是一个随机的小模式，是由验证将军启动的，但不知道是哪一个！如果你能认出这个名字，我会列出下面的一些次要模式。

如果我在Emacs中放置句点，光标将跳到它前面，如下所示：

写些东西 写些东西。 写些东西。

其中，|表示游标，最后两个行行依次发生。

如果在带句点的行的末尾单击，也会发生同样的情况。光标将出现在句点之后，并在句点之前立即跳转。

一些句子。(点击这里) 一些句子。| 一些句子。

最后两条线一条接一条地发生。

以下是次要模式的列表，以防您发现名称：

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...

Answer 1

证明通用与show-paren-mode不兼容。您可以使用M-x show-paren-mode关闭它，或者将(add-hook 'proof-ready-for-assistant-hook (lambda () (show-paren-mode 0)))放在.emacs中的适当位置。

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