status bar would be too small and wouldn't allow newlines, modals would need closing
for printing documentation and metavariables, I have been using virtual text documents, because the Idris 1 IDE provided syntactic highlighting for those. I think that would be too heavy for this. I'm tempted to switch all the Idris 2 docs to the output channel too, since there isn't any semantic highlighting yet, and it is more convenient than the virtual docs.
Change
https://github.com/meraymond2/idris-vscode/issues/71
Allows
:type-of
and:type-at
to be called as commands, so they can be assigned to keyboard shortcuts. At the moment, they're only available on hover.Output
I've gone with the output-channel to display the types. There are multiple ways of displaying information in VS, and none of them are great options.