Conceal subscripts in Coq syntax

Question

Some context and setup

I've been using Coq lately and the excellent coqtail plugin for syntax and proof development. I've seen some folks using Proof General in Emacs for a similar environment, and it conceals numbered subscripts, with

x0

turning into

x₀

Nifty, says I, and implements it in Vim:

" ~/.vim/after/syntax/coq/bk_extras.vim
for [digit, subscript] in [
      \ [0, '₀'],
      \ [1, '₁'],
      \ [2, '₂'],
      \ [3, '₃'],
      \ [4, '₄'],
      \ [5, '₅'],
      \ [6, '₆'],
      \ [7, '₇'],
      \ [8, '₈'],
      \ [9, '₉']]
  execute printf('syntax match coqSubscript /\%(\k\+\)\@<=%d\>/ containedin=ALLBUT,.*Comment,coqRequire conceal cchar=%s', digit, subscript)
endfor

And I source this code in ~/.vim/after/syntax/coq{,-{goals,info}}.vim with

runtime! syntax/coq/bk_extras.vim

---

The problem

There are a few, but they are pretty interrelated so I'll put them together. (If people object, I can split the questions out.)

• Numbers like 10 end up like 1₀, which makes sense based on the syntax pattern but not semantically. Is there a way to not match when the subscript is preceded by a number?
• Sometimes (and I can't figure out when) the subscripts don't conceal. That is, sometimes x0 will show as x₀ and others just x0. Example:

Is there a way to get all of them (and the H0s, etc.) to work? They seem to not conceal most often when the are followed by a (space or not) colon, if that helps.

Answer 1

Vim syntax is a beast. It takes some time to get used to it.

I suggest to try this:

scriptencoding utf-8

syn match coqSubscript keepend /\K\d\+/ms=s+1 transparent contains=coqSubscriptDigit
    \ containedin=ALLBUT,coqComment,coqRequire,coqSubscript,coqSubscriptDigit
syn match coqSubscriptDigit /0/ contained conceal cchar=₀
syn match coqSubscriptDigit /1/ contained conceal cchar=₁
syn match coqSubscriptDigit /2/ contained conceal cchar=₂
syn match coqSubscriptDigit /3/ contained conceal cchar=₃
syn match coqSubscriptDigit /4/ contained conceal cchar=₄
syn match coqSubscriptDigit /5/ contained conceal cchar=₅
syn match coqSubscriptDigit /6/ contained conceal cchar=₆
syn match coqSubscriptDigit /7/ contained conceal cchar=₇
syn match coqSubscriptDigit /8/ contained conceal cchar=₈
syn match coqSubscriptDigit /9/ contained conceal cchar=₉

UPD. Subscripts will not be shown within coq-goals syntax, coq-hypothesis region. The reason is the region start is defined with matchgroup=coqIdent. From :h :syn-matchgroup:

In a start or end pattern that is highlighted with "matchgroup" the contained items of the region are not used. This can be used to avoid that a contained item matches in the start or end pattern match.