Breaking with after/syntax directory about coqtail HOT 5 CLOSED

Thanks for reporting this. There are two issues that prevent your syntax rules from working.

First, you have to add coqprime to the coqTerm syntax group since most of the top-level syntax rules use contains=@coqTerm.

syn cluster coqTerm add=coqprime

Second, forall and fun are defined as keywords in Coqtail's syntax/coq.vim, which have higher priority than matches (:h syn-keyword). As far as I know, the only way to have your rules take precedence is to also define them as keywords.

syn keyword coqprime forall conceal cchar=∀
syn keyword coqprime exists conceal cchar=∃
syn keyword coqprime fun conceal cchar=λ

from coqtail.

Thanks for your help. I had a suspicion about the latter "keyword" priority vs. match part, but I had no idea about syntax groups/clusters. Thanks for showing me, and thanks for teaching me about syntax groups!

from coqtail.

Oh: there is a funny issue now where the concealed symbols have Normal bg when they instead should have CoqtailChecked:

I have yet to look into this but might you know how to resolve this?

from coqtail.

I'm not sure how or if there's a way to fix that. The CoqtailChecked highlighting is added with matchadd, which the Vim docs say should always have priority over syntax highlighting (:hi), but it seems like conceal may work differently. I found these links confirming other people have this issue, but no solutions as far as I can tell.

https://stackoverflow.com/questions/24131474/can-i-fix-conceal-highlight-group-background-in-highlighted-lines
https://vi.stackexchange.com/questions/26742/how-to-overwrite-the-conceal-background-color-with-line-color

from coqtail.

I see, thanks! I think I will stick with not concealing; I don't even know how I got so committed to this rabbithole in the first place. Thanks for your help.

from coqtail.