时间戳

首页 > 解决方案 > 在 Emacs 中使用 Coq 时，如何在 ProofGeneral 中自定义命令和战术的颜色？

emacs - 在 Emacs 中使用 Coq 时，如何在 ProofGeneral 中自定义命令和战术的颜色？

问题描述

我想将一些特定的命令和战术着色成不同的颜色，例如我希望“打印”和“定位”命令是灰色的，而“感应”是一些不同于其他战术的特殊颜色。

这在 ProofGeneral 中可能吗？如果它在 ProofGeneral 中不可配置，那么是否可以通过某些 Emacs 机制对其进行配置？

PS：我检查了ProofGeneral 的手册，但找不到任何相关选项。

标签： emacscoqcoqideproof-generalcoq-plugin

解决方案

据我所知，这在 ProofGeneral 中是不可能的。face但是，您可以通过在 emacs 中更改关键字来自定义关键字的颜色。为此，请将光标移动到您要更改的单词，然后按M-x并输入customize-face，这将带您进入自定义窗口。

要将关键字添加到 ProofGeneral 次要模式，您可能需要查看https://www.gnu.org/software/emacs/manual/html_node/elisp/Customizing-Keywords.html

这会添加induction带有字体锁定警告面的关键字

(add-hook 'coq-mode-hook
  (lambda ()
    (font-lock-add-keywords nil
      '(("\\<\\(induction\\):" 1 font-lock-warning-face prepend)))))

推荐阅读