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
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
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
10end 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
x0will show as
x₀and others just
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.