leanprover
Widgets: Emacs
While the main user of the new lean4-infoview is VSCode, the package is intentionally designed to be more or less independent of VSCode, needing only a connection to some editor functionality and the LSP server. This is so that other editors can implement the infoview. This issue is to track any potential progress on an Emacs implementation.
One possible (certainly really oversimplified) way that could go is as follows. The infoview is a webpage, so it needs a browser engine. Emacs-webkit could be used for this. The Emacs extension would start a Webkit webview and render the infoview into it. It would then have to set up message-passing with the webview in order to implement the editor API. This will likely want to use webkit--register-script-message. See also "User script messages" here and the code used to set up message passing in VSCode.
