Use case as vscode-style plugin for ace?

[glangmead]

What would it take to adapt this repo into an ace plugin which, unlike the ace integration in mkleanbook, can point to an instance of C++ lean running on a server? It seems lots of work has already been done to make ace into somewhat of a container for a language server protocol client plugin, given the integration I see in mkleanbook. I'd just like that one last piece which is to bypass the javascript version of lean and use whatever version I've compiled.

[gebner]

What would it take to adapt this repo into an ace plugin which [..] can point to an instance of C++ lean running on a server?

1. Write a WebSocket server that exposes stdin/stdout of the C++ server to the internet.
2. Add a WebSocketTransport/WebSocketConnection that connects to the server in 1.
3. Look at the ace code in https://github.com/gebner/gitbook-plugin-lean/blob/master/src/index.tsx

I'm not sure how we'll integrate the lean-client-js-browser package. I don't really want to touch the mkleanbook code too much. The new gitbook-based reference manual (where we could use gitbook-plugin-lean) hasn't really taken off yet either.

Maybe it would be a nice step forward to implement a standalone editor using the new lean-client-js library (like https://leanprover.github.io/programming_in_lean/?live).