whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
271 stars 35 forks source link

Feature Request: Conceal Common Coq Symbols #370

Open keikun555 opened 2 weeks ago

keikun555 commented 2 weeks ago

company-coq for emacs has concealment.

We could also conceal for vim coq syntax.

conceal                                         conceal :syn-conceal

When the "conceal" argument is given, the item is marked as concealable.
Whether or not it is actually concealed depends on the value of the
'conceallevel' option.  The 'concealcursor' option is used to decide whether
concealable items in the current line are displayed unconcealed to be able to
edit the line.
Another way to conceal text is with matchadd().
whonore commented 1 week ago

I'd be happy to accept a PR for this if you have the time and motivation. Otherwise, I'll try to get to it in the near future. One point to consider though is what to conceal and what symbols to replace them with. Most of the general symbols and the greek letters seem fairly uncontroversial, but I'm less sure about the miscellaneous ones. Perhaps there should be an option that controls which sets of symbols get concealed.