Implements two of the new commands added in Idris 2.
Type At is a variation of Type Of that handles local variables properly, so it's much more useful. The hover behaviour is already configurable (because the type-of works so badly, I wanted people to be able to disable it), so to use the new version, you just have to change the settings. I'm going to leave Type Of as the default in order not to break hover for Idris 1.
Generate Definition is an über-completion command that for a given function signature provides all of the possible cases along with solutions. Its use is the same as Add Case.
There's one problematic side effect with the way Generate Definition works that I don't have an answer for at the moment. Idris 2 has the ability to generate multiple possible solutions, which you can access with the IDE command :generate-def-next. But, it holds those solutions in its internal state, which is reset if the file is reloaded. And at the moment the file is reloaded whenever it's saved, in order to update the errors. In short, by the time the user can ask for the next definition through vscode, it won't be available.
I've looked at displaying the result of Generate Definition in some other way than inserting it into the source file. I could use the output pane or a virtual document. I'd prefer it closer to the original function declaration, like Sublime's phantom text, but I don't think VS supports anything like that. Another alternative would be to just always fetch an arbitrary number of extra definitions and save them to the VS state, and allow the user to cycle through those definitions. Doing 10 :generate-def-next doesn't add a noticeable delay. Either way, I'll keep the current implementation as the default, so it acts like all the other commands, and implement any other method as an additional command.
Implements two of the new commands added in Idris 2.
Type At is a variation of Type Of that handles local variables properly, so it's much more useful. The hover behaviour is already configurable (because the type-of works so badly, I wanted people to be able to disable it), so to use the new version, you just have to change the settings. I'm going to leave Type Of as the default in order not to break hover for Idris 1.
Generate Definition is an über-completion command that for a given function signature provides all of the possible cases along with solutions. Its use is the same as Add Case.
There's one problematic side effect with the way Generate Definition works that I don't have an answer for at the moment. Idris 2 has the ability to generate multiple possible solutions, which you can access with the IDE command
:generate-def-next. But, it holds those solutions in its internal state, which is reset if the file is reloaded. And at the moment the file is reloaded whenever it's saved, in order to update the errors. In short, by the time the user can ask for the next definition through vscode, it won't be available.I've looked at displaying the result of Generate Definition in some other way than inserting it into the source file. I could use the output pane or a virtual document. I'd prefer it closer to the original function declaration, like Sublime's phantom text, but I don't think VS supports anything like that. Another alternative would be to just always fetch an arbitrary number of extra definitions and save them to the VS state, and allow the user to cycle through those definitions. Doing 10 :generate-def-next doesn't add a noticeable delay. Either way, I'll keep the current implementation as the default, so it acts like all the other commands, and implement any other method as an additional command.