[ new ] Add a GenerateDefNext code action

[mattpolzin]

The existing LSP GenerateDef code action will generate a list of possible definitions for a type declaration. An alternative mode of interacting with these generated definitions would be to cycle through them.

This PR introduces the GenerateDefNext code action which cycles through generated defs inline (a previous def is replaced when the next one is requested).

In order for this new functionality to work, we need to carry forward proof search state across file loading. As best I can figure, this should be fine and has no negative impact on other existing LSP functionality, but there is definitely a possibility of regression in this area so we should be cognizant of the potential need to undo this change. If needed, the state needed for this GenerateDefNext code action could also be stored in LSP specific state instead of repl state.

[srghma]

I see You are member of https://github.com/idris-community - You could just merge it 😉

[andorp]

I think this is a good improvement. The generate 10 defs was a placeholder and I am really glad that you implemented the generate next def.

@mattpolzin
I don't have an active Idris installation at the moment, I can't really test this change, I trust it works for you. Just merge the PR whenever is the best.