On Monday, July 22, 2019 at 1:04:34 AM UTC+3, Mario Carneiro wrote: > > I can in principle do anything listed here: > > > https://code.visualstudio.com/api/language-extensions/programmatic-language-features > > Let me know if you see anything that would fit well with the proof > authoring experience. >
It seems that text formatting could be useful to provide some visual feedback. Another option which Lean uses but doesn't fall under any standard vscode > feature is to have a "goal view" which pops up on the right side of the > screen and basically shows you the result of (stat) continuously. To do > this I would have to extend the vscode extension, which I am loath to do > because it decreases the portability of the extension. Currently all the > work is being done from mm0-hs as a backend server and communication goes > via the language server protocol, which means that it should be easy to set > up a similarly featureful editor mode for any other LSP supporting editor, > such as emacs. > Sure, that's reasonable. I think that using VSCode's webview should also be ruled out as non-portable. Though, I can't help but think about elisp integration. Also Plan9 interface comes to mind where any text is in fact a widget. >> > > Could you elaborate on this? I haven't used Plan9, what's the interaction > story there? > In Plan 9 everything is a server, so its text editor Acme is a server which can interpret ranges of text as a message. So, you could just type something like "Open" in one of its buffers and use special mouse click to send it as a message to Acme server which opens a file. In fact the idea comes from Oberon and is described here <https://en.wikipedia.org/wiki/Oberon_(operating_system)#User_interface>. But I don't know if that's possible with LSP. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4a536d40-9daf-4227-93f1-cfa4441abed5%40googlegroups.com.
