On Sun, Jul 21, 2019 at 6:54 PM vvs <[email protected]> wrote: > 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. >
What do you mean? Are you talking about an MM1 code formatter (i.e. fixing spacing and indentation)? This is actually probably going to happen, because MM1 needs a formatter anyway since it outputs MM0 files and they have to be readable. There is already an expression pretty printer that displays subproof statements in the squiggles on "_" holes. (Try getting a big expression to print, over 80 chars, and it should do indentation and alignment and all that.) > > 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. > I recall back in the days before the lean goal view, it would instead post the goal view to "output", which is a command line style streaming view. You just put a "-------------------" before the goal statement, and post the goal every time the user types a character, and bam you've got a live updating view. It's a really low tech option which makes it much more portable. > 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. > Okay, after this and some research I have a sense of what this looks like. But how would you use something like this in MM1? What kind of interactions are you considering? Something that comes close to this is the "code action" feature. If you type the right text (something that the LSP server decides deserves a code action), vscode will pop up a lightbulb next to the text, and if you click on it you can perform some set of actions. Usually this is used in programming languages for doing refactoring operations: you click on a variable name, the lightbulb pops up, you find "export to method" or similar in the dropdown and click on it, and the server updates the content of the file with the result of the refactoring. Notice that this is changing the text area itself. While I think that excessive programmatic changing of the text area as in mmj2 is problematic, local changes can be used to simulate many of the things that mmj2 does. So for instance you could inline a tactic: Let's say (equality) is a tactic for discharging equality proofs. If you call it directly, then it proves the equality goal, but the lightbulb appears on it, and you can click the "inline tactic" button and it replaces "(equality)" in the file with "'(eqeq1d (oveq1d (oveq2)))" or whatever the equivalent direct proof would be. This is not always a valid move, for instance if the lisp program also has some side effects like adding new definitions and so on, but I imagine that many tactics will fit this mode of operation, and as long as the user is in the driver's seat here they can choose to use it only when it is applicable. -- 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/CAFXXJSv2dfap9vnpkvVbnjDN_y3PQ6wo5kvFYHorN8V5iRyRGA%40mail.gmail.com.
