Closed RalfJung closed 4 weeks ago
It would be great if either the existing shortcuts could be repurposed to also support a customizable query, or new shortcuts could be added to implement "jump to vscoq panel, select a given query type, fill the query text with the selected string, and put the focus in the query text field (with the entire field contents being selected so that I can easily overwrite them)".
FWIW the details can of course be different -- I am not sure what the best/idiomatic way to do such a "prompt" in vscode is. The key point is to be able to do something like "hit shortcut, type query (pre-filled sensibly), hit enter, see result".
ProofGeneral has this great feature that I use a lot:
About <string>
/Locate <string>
/Search <string>
.In vscoq, similar shortcuts exist, but they seem to only be able to search what I have selected -- I can't type my own query. To type my own query, I have to switch my right hand to the mouse, open the vscoq panel, select the desired query type, select the query text field, type the query, and hit enter -- that takes so long that I'd rather just type
About <string>.
into the editor.It would be great if either the existing shortcuts could be repurposed to also support a customizable query, or new shortcuts could be added to implement "jump to vscoq panel, select a given query type, fill the query text with the selected string, and put the focus in the query text field (with the entire field contents being selected so that I can easily overwrite them)".