Hi Ara,
I don't know what's planned for Blodwen, but I'll share some
perspective as a major implementor of current-Idris's editor
interactions.
While Idris's editor integration predates the VS Code LSP, I still
think I'd be hesitant about adopting it. In order to get the kind of
experience that I wanted to have, it would require lots and lots of
extensions, to the point where it's not really fair to say that one is
using the same protocol. LSP has features that Idris doesn't, which is
fine, but Idris also has lots of features not covered by LSP. While
LSP is a reasonable floor to get the very basic stuff working quickly,
it seems to be also setting a ceiling for everyone's ambitions these
days.
Here's some examples of where they don't match well:
* LSP specifies that text is sent as only plain text or Markdown.
Idris supports rich semantic annotations on text from the compiler,
giving things like doc summaries, type signatures, and handles that
can be used for interaction with the underlying information
represented by the string. Consequences of this are the semantic
highlights, the ability to have interactive examples in docs (e.g,
right-click on the example to get it evaluated in place), and
interactive error messages. It'd be a shame to give those things up.
* LSP doesn't have any notion of "holes" in a program, but getting the
hole list is an important part of type-driven editing.
* LSP still doesn't have a way for the compiler to highlight the
source document based on the semantics of each substring. It's not
clear that there even is one protocol for that that's reasonable for
different languages - Idris sends highlighting as a "push" as a side
effect of type checking, while other languages may work better if the
editor "pulls" highlighting when scrolling around.
* LSP hard-codes UI features of VS Code, like "code lens" and "hover",
rather than talking about the meaning of documents. The Idris protocol
instead has things like "what is the type" and "what are the docs".
This is a place where Idris's protocol enables a wider variety of UIs.
This is a way in which LSP is significantly less flexible. Imagine if
the Idris protocol hardcoded imenu and the Emacs minibuffer!
* LSP doesn't contain commands for REPLs, nor for things like case-splitting.
There's a bunch more. It would be reasonable to define lots of
extensions to "LSP" to get back up to where the current Idris UIs are,
but these would still require lots of implementation in each editor. I
think the big benefit of using the VS Code protocol would be that an
extremely basic experience would be quickly available, but almost all
the work is in the parts that go beyond what LSP offers anyway. The
other big benefit is that LSP wants compilers to be structured in a
certain way, and I think that redoing Idris/Blodwen in that way would
be an improvement. I'd almost rather see a better protocol for
languages like Idris, Agda, and Lean that could be supported directly.
If those extensions ever do get made to LSP, it'd be straightforward
to retarget at least the Emacs mode. Most of the code is not
particularly tied to the protocol - it's about displaying appropriate
UIs and such.
David