Default Keyboard Shortcuts

[namuol]

It might be nice to use all the default keyboard shortcuts in the official Idris book (for consistency with the Atom plugin):

Shortcut	Command	Description
Ctrl-Alt-A	Add definition	Adds a skeleton definition for the name under the cursor
Ctrl-Alt-C	Case split	Splits a definition into pattern-matching clauses for the name under the cursor
Ctrl-Alt-D	Documentation	Displays documentation for the name under the cursor
Ctrl-Alt-L	Lift hole	Lifts a hole to the top level as a new function dec- laration
Ctrl-Alt-M	Match	Replaces a hole with a case expression that matches on an intermediate result
Ctrl-Alt-R	Reload Search	Reloads and type-checks the current buffer
Ctrl-Alt-S	Type-check name	Searches for an expression that satisfies the type of the hole name under the cursor
Ctrl-Alt-T	Description	Displays the type of the name under the cursor
Ctrl-Alt-W	with block insertion	Adds a with block after the current line, contain- ing a new pattern-matching clause with an extra argument

[petermarks]

+1.

If you are reluctant to enforce this, at least it would be nice to include the necessary config in the plugin's home page/readme so users could just copy and paste.

Here is what I use which doesn't match namuol's list completely, but is close:

{
"key": "ctrl+alt+a",
"command": "idris.add-clause",
"when": "editorTextFocus && editorLangId == idris"
},
{
"key": "ctrl+alt+c",
"command": "idris.case-split",
"when": "editorTextFocus && editorLangId == idris"
},
{
"key": "ctrl+alt+m",
"command": "idris.make-case",
"when": "editorTextFocus && editorLangId == idris"
},
{
"key": "ctrl+alt+r",
"command": "idris.typecheck",
"when": "editorTextFocus && editorLangId == idris"
},
{
"key": "ctrl+alt+s",
"command": "idris.proof-search",
"when": "editorTextFocus && editorLangId == idris"
},
{
"key": "ctrl+alt+t",
"command": "idris.type-of",
"when": "editorTextFocus && editorLangId == idris"
},
{
"key": "ctrl+alt+w",
"command": "idris.make-with",
"when": "editorTextFocus && editorLangId == idris"
},
{
"key": "ctrl+alt+x",
"command": "idris.start-refresh-repl",
"when": "editorTextFocus && editorLangId == idris"
}

Also, I personally don't like the clutter on the context menu. Could there be an option to disable adding the commands there?

[DejanMilicic]

@petermarks any idea how to return the cursor to file after executing any of these commands? It is quite tedious to execute a command via shortcut and then reach for to mouse just to be able to continue typing...

[vzhn]

@DejanMilicic ctrl-1 returns cursor to the file in the first tab