ProofGeneral
replacing old adhoc `holes` by `yasnippet`?
Among other things, PG coq can builds tons of abbrevs from coq-syntax.el databases (which I should update by the way). This abbrevs can optionally make use of "holes" which provide standard code template features + a poor man's structural edition mechanism (of which I am probably the only user). This can be tested this by typing heC-x' and then C-c C-j to jump from one hole to the next one.
yasnippet is quite standard nowadays for code templates. It is already used by company-coq (but for very few templates afaiu @cpitclaudel can you confirm?). It is much more robust and tested. It has less structural edition features than holes.el but I think nobody cares.
I am considering adding yasnippet support from coq-syntax.el databases. Once this works I will remove holes.el.
Things to check:
- [ ] what happens if company-coq and pg play with yasnippets?
- [ ] Does anyone use holes except me?
- [ ] propose one or two changes to strange entries in
coq-syntax.elconcerning ssreflect commands @amahboubi. - [ ] decide if we should propose a small set of templates instead of hundreds of them.
Remarks welcome.
I don't use holes. Company-Coq currently uses yasnippet; it has a bit over 1000 templates. These templates are automatically extracted from the manual. Here's the complete list: https://github.com/cpitclaudel/company-coq/blob/master/company-coq-abbrev.el
Indeed I didn't realize your nice completion mechanism was already using yasnippet. Can you explain how it interacts with regular yasnippet minor mode? It seems to live separately (which is fine I think). For instance when I use yas-expand it does not use comany-coq's snippets, you snippet do not appear int yasnippet menu, etc.
What would be the best place to poll PG users?
Can you explain how it interacts with regular yasnippet minor mode?
Yes: it inserts snippets from a company-mode post-completion action, see https://github.com/cpitclaudel/company-coq/blob/4da7b41e25943c0e30171ed25c761c5311999f0d/company-coq.el#L2690