Does the LSP for Lean4 include comms with external app?

Stream: general

[Daniel Donnelly]

Was wanting to make a a 3D viewer in the D language for 3D box-like commutative diagrams. Was wondering how much it can interact with what the Lean4 user is doing in the proof. For instance if they draw in an arrow with a mouse, then we declare a variable under the hypotheses via a "let f:A ->B be a morphism in our category C". Possible or not quite at the moment?

[Kim Morrison]

Yes, things like this are completely possible, but obviously significant work. You can run javascript in the infoview, and have bidirectional communication with the Lean state.