How to customize colors for Command and Tactic in ProofGeneral when using Coq in Emacs?

Question

I want to color some specific command and tactic into different color, e.g. I want "Print" and "Locate" command to be gray, and "induction" to be some special color different from other tactics.

Is this possible in ProofGeneral? If it is not configurable in ProofGeneral, then is it possible to configure it via some Emacs mechanism ?

PS: I have checked the manual of ProofGeneral, but cannot find any related option.

Answer 1

As far as I know, this is not possible in ProofGeneral. However, you can customize the colour of keywords by changing their face in emacs. To do this, move the cursor to the word you want to change and then press M-x and enter customize-face, which will bring you to the customization window.

To add keywords to the ProofGeneral minor mode, you may want to have a look at https://www.gnu.org/software/emacs/manual/html_node/elisp/Customizing-Keywords.html

This adds the induction keyword with the font-lock warning face

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