I'm pretty torn, on the one hand this tight vscode integration should exist, and is being used to good effect by projects like the lean info-view, which shows t

I'm pretty torn, on the one hand this tight vscode integration should exist, and is being used to good effect by projects like the lean info-view, which shows the goals of the proof state. And my own project which e.g. generates railroad diagrams and displays them in the editor. On the other hand, it is kind of unfortunate that this sort of tight integration with language server and editor is happening in the editor which drives/governs the specification itself. I think it would be much more tolerable in regards to the future of the specification if these sorts of "above and beyond" integrations were all happening in any other editor.