Stream: Proof General users

Topic: ✔ Emacs Theme config


view this post on Zulip Clément Blaudeau (Dec 13 2021 at 22:14):

Hi everyone! I'm using Coq with ProofGeneral on Emacs (+CompanyCoq), but with a dark theme. I've managed to change the color of locked regions to be pleasant with my theme (proof-colour-locked). The only thing missing is the color of regions that are "in-processing", typically when some tactics take a few seconds to go through. Does someone know the parameter I need to change ? I'm not sure if this setting comes from PG or from Emacs itself by the way.
Thank you !

view this post on Zulip Clément Blaudeau (Dec 29 2021 at 14:12):

Found it. It's the Proof Queue Face setting of Proof general.

view this post on Zulip Notification Bot (Dec 29 2021 at 14:12):

Clément Blaudeau has marked this topic as resolved.

view this post on Zulip Pierre Courtieu (Jan 21 2022 at 14:28):

Non exhaustive examples of font setting for PG and company-coq:

 `(proof-error-face ((t (:underline (:color "red" :style wave)))))
   `(proof-warning-face ((t (:background "DarkRed"))))
   `(proof-eager-annotation-face ((t (:underline (:color "red" :style wave)))))
   `(proof-locked-face  ((t (:background "#323255"))))
   `(proof-queue-face  ((t (:background "#351919"))))
   `(coq-solve-face  ((t (:foreground "red3"))))
   `(proof-tactics-name-face  ((t (:foreground "#cb92ff"))))
   `(company-coq-features/code-folding-bullet-face ((t (:inherit link :bold t :underline nil))))
   `(proof-declaration-name-face  ((t (:bold t :foreground "orange")))) ;;

   ;`(diff-refine-changed ((t (:background "#aaaa22"))))
   ;`(diff-refine-added ((t (:background "#aaaa32"))))
   `(coq-diffs-added-face ((t (:background "#225522"))))
   `(coq-diffs-added-bg-face ((t (:background "#203020"))))
   ```

Last updated: Feb 06 2023 at 05:03 UTC