0

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:

Interactive Coq session with some x0 concealed to x₀ and others not

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.

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.

6
  • Would this turn all digits into subscripts? Neat. I'll have to try it. – D. Ben Knoble Feb 12 at 18:19
  • This fixes the number issue, but doesn't help with the colons, where in the screenshot H0 : and x0 : do not conceal (the coq-goals pane, but in other places too). – D. Ben Knoble Feb 12 at 20:15
  • @D.BenKnoble Not sure which one. But you should anyway check what is the syntax item underneath. Maybe it's that "coqRequire" you've excluded for some reason. – Matt Feb 12 at 20:19
  • No, it's coqIdent that seems to be the issue, but that's not excluded – D. Ben Knoble Feb 12 at 20:22
  • @D.BenKnoble Updated. This is an issue with original syntax file. – Matt Feb 13 at 6:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.