PUMPKIN-PATCH icon indicating copy to clipboard operation
PUMPKIN-PATCH copied to clipboard

What should the UI for refactoring be?

Open samuelgruetter opened this issue 4 years ago • 0 comments

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.

samuelgruetter avatar Nov 14 '19 20:11 samuelgruetter