-
Notifications
You must be signed in to change notification settings - Fork 7
Open
Description
以下のような設定で、
(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