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 !
Found it. It's the Proof Queue Face
setting of Proof general.
Clément Blaudeau has marked this topic as resolved.
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: Oct 13 2024 at 01:02 UTC