Skip to content

auto-complete-mode併用時、post-command-hookでのエラー #31

@zk-phi

Description

@zk-phi

以下のような設定で、

  (defun my-coq-smart-pipes ()
    "insert pipe surrounded by spaces, and reindent"
    (interactive)
    (if (looking-back "\\[")
        ;; empty list delimiter
        (insert "| ")
      ;; guard
      (insert (concat (if (looking-back " ") "" " ")
                      "|"
                      (if (looking-at " ") "" " "))))
    (save-excursion (smie-indent-line)))

  (defun my-install-coq-smartchr ()

    (key-combo-define-local (kbd "|") '(my-coq-smart-pipes))
    (key-combo-define-local (kbd ":") '(" : " " :: "))
    (key-combo-define-local (kbd ":=") " := ")
    (key-combo-define-local (kbd "=") " = ")

    (key-combo-define-local (kbd "->") " -> ")
    (key-combo-define-local (kbd "<-") " <- ")
    (key-combo-define-local (kbd "/\\") " /\\ ")
    (key-combo-define-local (kbd "\\/") " \\/ ")
    (key-combo-define-local (kbd "|-") " |- ")
    (key-combo-define-local (kbd "|=") " |= ")

    (key-combo-define-local (kbd "=>") " => ")
    (key-combo-define-local (kbd ":<") " :< ")
    (key-combo-define-local (kbd ":>") " :> ")

    (key-combo-define-local (kbd "<") " < ")
    (key-combo-define-local (kbd "<=") " <= ")
    (key-combo-define-local (kbd ">") " > ")
    (key-combo-define-local (kbd ">=") " >= ")
    (key-combo-define-local (kbd "+") '(" + " "+"))
    (key-combo-define-local (kbd "-") '(" - " "-"))
    (key-combo-define-local (kbd "*") '(" * " "*")))

次のようなコードを入力しようとした際、

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.

->の「>」を入力したタイミングでエラー、「Changes to be undone are outside visible portion of buffer」が起こりました。post-command-hookを使っているプラグインをそれぞれ外して試してみたところ、どうやらauto-complete-modeとの併用時に問題が起こるようです。実際、auto-complete、key-combo、coq-mode(proof general)のみがインストールされたemacs 23.3で同様のエラーが起こることを確認しました。また、auto-completeのac-auto-startをnilにし補完が行われないよう設定すると、問題は起こらなくなりました。

どちらも重宝しているプラグインなので、なんとか両立ができるとありがたいなと思います。
確認お願いいたします。

Metadata

Metadata

Assignees

Labels

No labels
No labels

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions