5

我正在尝试将 coq 与 ProofGeneral 一起使用，但内置的 Verilog 模式会影响*.v文件类型识别。我可以以某种方式禁用它并让 ProofGeneral 将它们重新映射到它的 coq 模式吗？

4

4 回答 4

5

您将不得不在您的 .emacs 或其他文件中覆盖 auto-mode-alist 中的绑定。

这篇 SO 帖子与 VHDL 做了类似的事情：

如何在 emacs 中关闭 vhdl 模式？

另外，我搜索了“auto-mode-alist remove”并找到了这个链接。复制/粘贴重要部分：

;; Remove all annoying modes from auto mode lists

(defun replace-alist-mode (alist oldmode newmode)
  (dolist (aitem alist)
    (if (eq (cdr aitem) oldmode)
    (setcdr aitem newmode))))

;; not sure what mode you want here. You could default to 'fundamental-mode
(replace-alist-mode auto-mode-alist 'verilog-mode 'proof-general-mode)
于 2012-03-08T21:41:51.540 回答
2

我不熟悉 ProofGeneral，但如果我正确理解您的问题，您需要修改auto-mode-alist变量以将正确的专业与具有.v扩展名的文件相关联。因此，您需要在文件中添加类似这样的.emacs内容：

(add-to-list 'auto-mode-alist '("\\.v$" . proof-general-coq-mode))
于 2012-03-08T21:39:21.897 回答
1

以下行有效：

(setq auto-mode-alist (remove (rassoc 'verilog-mode auto-mode-alist) auto-mode-alist))
于 2012-03-08T21:48:48.493 回答
1

这可能是一个 XY 问题。

我今天遇到了同样的问题，首先，我尝试了和你一样的东西，我在下面添加了以下~/.spacemacs内容dotspacemacs/user-init：

(setq auto-mode-alist (remove (rassoc 'verilog-mode auto-mode-alist) auto-mode-alist))

然后mode就变成了基础，然后我才意识到，真正的原因是spacemacs coq层没有自动安装，你需要花费很多精力来安装它，并且它的依赖关系很好。

以下是我在 Emacs 上成功运行 Coq 后对安装步骤的总结： https ://gist.github.com/luochen1990/68e5e38496b79790e70d82814bdfc69a

希望这有帮助:)

于 2019-09-20T13:14:07.327 回答