Feedback on VSCode extension

[mbbarbosa]

This is a placeholder for feedback on the VS Code extension.

First feedback:
=> "run to" is a bit brittle
-> cannot seem to "run to" a previous location
-> if a tactic fails, not clear where we are in the proof, in particular there is no location info
=> often parse error is reported but it seems to be just an exception state for the extension
=> seems quite a bit slower than emacs mode
=> it would really help to have menu entries (or a clickable context menu)
to understand what actions we can do and what are the
shortcuts