Request: electric bullets

[jonleivent]

Since Coq now tells us which bullet to use to focus the next subgoal (via response "Focus next goal with bullet X." when a goal is completed), can Company-Coq use that so that typing "-" to start the new goal will automatically get changed to the correct bullet?

For extra credit, can Company-Coq figure out which bullet to use when focusing on a subgoal of the current goal? Again via typing "-" as above. That would require knowing the bullet that started the current goal, and which comes next in the progression.

For even more credit, can Company-Coq figure out when to close off a finished subgoal that started with "{" with "}"?

[cpitclaudel]

Interesting ideas! It sounds tricky, though. In particular, I don't think we'll be able to bind it to -, since that - could also be part of a notation (such as ->, or minus itself). Given that, I'm not sure how we'll get users to discover the feature.

On the other hand, the curly brace closing idea could work; but I wonder if we can fully get ride of false positives; they will be very annoying.

I'd be happy to merge a relatively simple implementation, but I'm not sure I can dedicate it some time to this at the moment (in part because I don't use 8.5, so I wouldn't be able to give the feature enough testing).

[jonleivent]

Can company-coq detect when there are remain goals, but none are in focus? If so, then if "-" is bound to an electric bullet in that case but self-insert otherwise, that might work. Because when there are no goals in focus, no other notation is allowed. At least that would allow an electric bullet for the non-first subgoal cases - which are precisely the cases where the exactly proper bullet is required.

For the first subgoal, if one waits until the user has attempted to move the admitted region past the "-", and has received feedback from Coq that it is not the proper bullet to use, can company-coq undo and replace it with the proper bullet?

[cpitclaudel]

an company-coq detect when there are remain goals, but none are in focus?

I'm not too sure how; the goal display isn't always up-to-date.

For the first subgoal, if one waits until the user has attempted to move the admitted region past the "-", and has received feedback from Coq that it is not the proper bullet to use, can company-coq undo and replace it with the proper bullet?

That sounds a bit too magical to me :/ And indentation would have to be changed too.