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 like1₀
, 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 asx₀
and others justx0
. Example:
Is there a way to get all of them (and the H0
s, etc.) to work? They seem to not conceal most often when the are followed by a (space or not) colon, if that helps.