Cannot process just comments

[tchajed]

VsCoq seems to never process just a comment. I think this is a bug.

If you're going through a file with large comments (e.g., in class), then it's possible to lose track of where the interpretation is up to is because the current view only has comments. In Proof General I step through those comments and can see exactly where that point is.

Processing the first comment in the file is also how I confirm that Coq has started and things are working, which doesn't do anything in VS Coq. This is true even with Proof Interpretation Mode set to NextCommand; you have to put the cursor on the non-comment part of the first sentence.

This also affects backtracking: if you backtrack before a command, it also reverts any comments before the command. This also leaves it unclear exactly where the backtracking went to, if it goes off screen. I'd prefer the comment remain processed.