Support more commands

[zjhmale]

• IDE-Mode

• :add-proof-clause d238beb
• :add-missing
• :who-calls
• :calls-who
• :browse-namespace 54c7eab
• :normalise-term
• :show-term-implicits
• :hide-term-implicits
• :elaborate-term

• REPL

• :search 785126b

[zjhmale]

The :browse-namespace also need some enhancement, since there is not location information (file-path:line:column) with the result.

[philipcraig]

Could who-calls be wired up to the Extension Find All References command, or does that not make sense?

[zjhmale]

Yeah, we don't really need some commands here, and some concrete commands still need some improvement itself. Thanks for the heads up.

Could who-calls be wired up to the Extension Find All References command, or does that not make sense?

[zjhmale]

BTW, who-calls command may be useful to help us implementing the find-usage feature.

[st3v3c00k]

I cannot see any keyboard shortcuts for the existing commands. Are they planned?

[zjhmale]

Hi @st3v3c00k, there used to be default key bindings for all the existing commands but then I removed them in order to avoid introducing any key binding conflicts. So you can call them using right click dropdown menu, using command palette or add command key bindings by youself in keybindings.json setting file.

[st3v3c00k]

Thanks.