PUMPKIN-PATCH
PUMPKIN-PATCH copied to clipboard
What should the UI for refactoring be?
Here's one answer/vote: I think the UI for issuing refactoring commands should be just the language server protocol (https://langserver.org/), like this all editors supporting the protocol will be able to use your features. VSCode makes it easy to use the language server protocol, I think https://github.com/coq-community/vscoq does so.