Ramkumar Ramachandra
Ramkumar Ramachandra
Any progress on this?
I think PG achieves jumping-to-definition via a `TAGS` file generated by [coqtags](https://github.com/ProofGeneral/PG/blob/master/coq/coqtags).
I think you meant #266. I had a look at it, and we can consider postponing the prettier patch until that lands. While I agree that npm is not broken...
I would prefer F12 to mean jump-to-definition for consistency with the rest of vscode. Looks okay otherwise.
I've implemented some of the shortcuts in #93. I found that using F6 for step-forward, and F7 for step-backward was more convenient. F9 is for interrupt-process.
vscode already uses function-key shortcuts in many other languages. F5 is to start-debugging, Shift+F5 is to restart debugging, F12 is to goto-definition, Shift+F12 is to show references. While debugging, several...
Okay, so have you remapped goto-definition, or do you not use goto-definition at all? Which other function keys do you use on a regular basis? In the patch, I haven't...
Are you on a Mac? You could try Fn+F12 to jump-to-definition instead. The question then becomes more of: would you like to keep hitting Fn every time you debug, or...
Users don't _have_ to change their default behavior. There may be some gap in the communication, so let me clarify. If you don't change anything, the default keybinding for step-forward...
There's unfortunately no way to choose between different sets of keybindings. If you agree that these new keybindings would be preferred by people more well-versed with vscode, and if you're...